Changes between Version 7 and Version 8 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 1:49:05 PM (11 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v7 v8  
    33This page is to track design and implementation ideas around adding a form of dependent types to Haskell. This work will also fix bug #7961. Richard Eisenberg (a.k.a. goldfire) is expecting to take on most (all?) of this work. 
    44 
    5 == Surface Language Design == 
     5= Surface Language Design = 
    66 
    77It is possible to fix #7961 without any surface language changes, as that bug addresses only lifting restrictions on promotion. There is a chance that this bugfix will enter HEAD without all of the other features below, but this writeup generally will not consider fixing #7961 separate from adding dependent types. 
    88 
    9 === Merging Types and Kinds === 
     9== Merging Types and Kinds == 
    1010 
    1111Following the work in [#nokinds the kind equality paper], the new Haskell will merge types and kinds into one syntactic and semantic category. Haskell will have the `* :: *` property. As a consequence, it will be easily possible to explicit quantify over kinds. In other words, the following type signature is allowed: `forall (k :: *) (a :: k). Proxy a -> Proxy a`. Furthermore, kind variables will be able to be listed explicitly when declaring datatypes and classes. Of course, if a kind variable is listed explicitly in the declaration of a type or class, then it also must be listed explicitly at the use sites. Note that this change will completely eliminate `BOX`. 
    1212 
    13 === Quantifiers === 
     13== Quantifiers == 
    1414 
    1515As pointed out in the [#hasochism Hasochism paper], Haskell currently enjoys a confluence of design decisions. One says that compile-time arguments are elided in runtime code. For example, when calling `map :: (a -> b) -> [a] -> [b]`, the type instantiations for `a` and `b` are properly arguments to `map` (and are passed quite explicitly in Core), but these arguments are always elided in surface Haskell. As the levels are mixing, we may want to revisit this. Along similar lines, type arguments in Haskell are always erasable -- that is, instantiations for types are never kept at runtime. While this is generally a Good Thing and powers much of Haskell's efficiency, dependent typing relies on keeping ''some'' types around at runtime. Here, it is even more apparent that sometimes, we want to be able to pass in values for type arguments, especially if those values can be inspected at runtime. 
     
    2020||= Quantifier =||= Dependent? =||= Visible? =||= Required? =||= Relevant? =|| 
    2121|| `forall` || yes || unification || FVs || no || 
    22 || `->` || no || yes || yes || yes || 
     22|| `->` || no || as term || yes || yes || 
    2323|| `=>` || no || solving || yes || yes || 
    2424 
    2525* ''Dependent'' means that the quantified thing (henceforth, ''quantifiee'') can appear later in the type. This is clearly true for `forall`-quantified things and clearly not true for `->`-quantified things. (That is, if we have `Int -> Bool`, we can't mention the `Int` value after the `->`!) 
    26 * ''Visibility'' refers to whether or not the argument must appear at call sites in the program text. If something is not visible, the table lists how GHC is to fill in the missing bit at call sites. 
     26* ''Visibility'' refers to whether or not the argument must appear at call sites in the program text. If something is not visible, the table lists how GHC is to fill in the missing bit at call sites. If something is visible, we must specify how it is parsed, noting that the term- and type-level parsers are different. 
    2727* A ''required'' quantification is one that must textually appear in the type. Note that Haskell freely infers the type `a -> a` really to mean `forall a. a -> a`, by looking for free variables (abbreviated to FVs, above). Haskell currently does slightly more than analyze just free variables, though: it also quantifies over free ''kind'' variables that do not textually appear in a type. For example, the type `Proxy a -> Proxy a` really means (in today's Haskell) `forall (k :: BOX) (a :: k). Proxy a -> Proxy a`, even though `k` does not appear in the body of the type. Note that a ''visible'' quantifications impose a requirement on how a thing is used/written; ''required'' quantifications impose a requirement on how a thing's type is written. 
    2828* ''Relevance'' refers to how the quantifiee can be used in the term that follows. (This is distinct from dependence, which says how the quantifiee can be used in the ''type'' that follows!) `forall`-quantifiees are not relevant. While they can textually appear in the term that follows, they appear only in irrelevant positions -- that is, in type annotations and type signatures. `->`- and `=>`-quantifiees, on the other hand, can be used freely. Relevance is something of a squirrely issue. It is (RAE believes) closely related to parametricity, in that if `forall`-quantifiees were relevant, Haskell would lose the parametricity property. Another way to think about this is that parametric arguments are irrelevant and non-parametric arguments are relevant. 
     
    3333||= Quantifier =||= Dependent? =||= Visible? =||= Required? =||= Relevant? =|| 
    3434|| `forall (...) .` || yes || unification || FVs + Rel.I. || no || 
    35 || `forall (...) ->` || yes || yes || yes || no || 
     35|| `forall (...) ->` || yes || as type || yes || no || 
    3636|| `pi (...) .` || yes || unification || FVs + Rel.I. || yes || 
    37 || `pi (...) ->` || yes || yes || yes || yes || 
    38 || `->` || no || yes || yes || yes || 
     37|| `pi (...) ->` || yes || as term || yes || yes || 
     38|| `->` || no || as term || yes || yes || 
    3939|| `=>` || no || solving || yes || yes || 
     40 
     41Note that the current quantifiers remain and with their original meanings. This table adds three new quantifiers: `forall ->`, and the two `pi` quantifiers. The idea is that, currently, we always say `forall`, then some binders and then a `.`. If we replace the `.` with an `->`, then we make the quantifications ''visible'' but otherwise unchanged. (Quantification not mentioned in a type defaults to ''invisible'', thus making the visible quantification ''required''.) 
     42 
     43The new `pi` quantifiers allow for quantifiees that are both dependent and relevant. This means that the quantifiee is named in the type and can be used within its scope in the type, and also that the quantifiee can be inspected in the term.  
     44 
     45== Open design questions == 
     46 
     47=== Parsing === 
     48 
     49Parsing is a bit a nightmare for this new language and will require some compromises. 
     50 
     51* Merging types and kinds is almost straightforward, but for one major stumbling block: `*`. In a kind, `*` is parsed as an alphanumeric identifier would be. In a type, `*` is parsed as an infix operator. How can we merge the type- and kind-parser given this discrepancy? As an example, what is the meaning of `Foo * Int`? Is it the type `Foo` applied to `*` and `Int`? Or is it the operator `*` applied to `Foo` and `Int`? The solution to this annoyance seems to be to introduce a new identifier for `*` (say, `TYPE`) and then remove `*` from the language, allowing it to be used for multiplication, for example. 
     52  * What name to choose for `*`? `TYPE` would appear plenty in code, and it seems a little rude. Choosing a new symbol just kicks the can down the road. Choosing `Type` would conflict with lots of code (including GHC's) that uses a type `Type`. Choosing `T` would conflict with lots of (example) code that uses `T`. The best option I'm aware of is `U`, short for universe. Mitigating this problem somewhat is that Dependent Haskell would come with kind synonyms, and whatever name we choose would be a "normal" name exported from the `Prelude` and could be hidden if desired. 
     53  * What is our migration strategy? One proposal: introduce the new name now and keep `*` around. Then, when Dependent Haskell is ready for release, it will come with a new extension flag which will change the parsing of `*`. Only when that flag is enabled would `*` fail to work. It is unclear whether it is worth it to fully squash `*` out of the language. 
     54 
     55* The type language and the term languages are more different. Even if we could write some kind of combined parser, the renamer would have major trouble distinguishing between data constructors and type constructors. One way or the other, programmers will likely have to specify how to parse their arguments explicitly. Take `id :: forall a -> a -> a`. This is just like the normal `id`, but with the type parameter explicit. Because the parser/renamer won't know the type of `id` when parsing its arguments, the first argument will have to manifestly be a type. For example, `id @Bool True`. The `@` indicates to the parser that the following thing is a ''type'', not a ''term''. 
     56 
     57* We will similarly need a syntax for type patterns embedded within term patterns. It would be ideal if the pattern syntax were identical to the expression syntax. 
     58 
     59* The choice of `@` above is stolen from the ExplicitTypeApplication and TypeApplication proposals, neither of which have been implemented and will be subsumed by Dependent Haskell (if we get to that first). Is this the right choice, though? For example, the ExplicitTypeApplication page includes an example of ambiguity: 
     60 
     61  {{{ 
     62  f :: Int -> forall a. a 
     63  f n @a = .... 
     64  }}} 
     65 
     66  This is ambiguous because `@`-patterns allow a space around the `@`-sign. However, common usage does ''not'' use any spaces around `@`, and we could use the presence/absence of a space to disambiguate between an `@`-pattern and a type pattern. 
    4067 
    4168 
    4269 
    43  
    44 == Related work == 
     70= Related work = 
    4571 
    4672'''Readers:''' Please add to these lists! 
     
    4874There are several published works very relevant to the design: 
    4975 
    50 * [http://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds.pdf System FC with Explicit Kind Equality]. [=#nokinds Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg]. ICFP 2013. 
     76* [http://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds.pdf System FC with Explicit Kind Equality]. [=#nokinds Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg.] ICFP 2013. 
    5177* [https://personal.cis.strath.ac.uk/adam.gundry/thesis/thesis-2013-07-24.pdf Type Inference, Haskell, and Dependent Types]. Adam Gundry. PhD Thesis, 2013. 
    5278 
     
    5480 
    5581* [http://www.cis.upenn.edu/~eir/papers/2012/singletons/paper.pdf Dependently typed programming with singletons]. Richard A. Eisenberg and Stephanie Weirich. Haskell Symposium 2012. 
    56 * [https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf Hasochism: The Pleasure and Pain of Dependently Typed Haskell]. [=#hasochism Sam Lindley and Conor !McBride]. Haskell Symposium 2013. 
     82* [https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf Hasochism: The Pleasure and Pain of Dependently Typed Haskell]. [=#hasochism Sam Lindley and Conor !McBride.] Haskell Symposium 2013.