Changes between Version 8 and Version 9 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 2:06:40 PM (10 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v8 v9  
    4141Note 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''.) 
    4242 
    43 The 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.  
     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. A `pi`-bound argument is a proper dependent type. Since a `pi`-quantifiee can appear in both terms and types, its instantiations must come from a restricted subset of Haskell that makes sense at both the type and term level. This issue is addressed in [#gundry Adam Gundry's thesis]. For now, we propose that this subset include only data constructors (perhaps applied) and other `pi`-quantifiees. The subset can be expanded later. For some tantalizing ideas of how far it can go, see [#promotion this paper], discussing promotion of Haskell terms to types. 
    4444 
    4545== Open design questions == 
     
    6666  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. 
    6767 
     68=== Overriding visibility defaults === 
    6869 
     70The `.`/`->` distinction in quantifiers allows programmers to specify the visibility of arguments at use sites. But, sometimes callers will want to override the defaults. 
     71 
     72* If a visible, dependent argument is to be elided, we could allow `_` to indicate that GHC should use unification to fill in the argument. (This is similar to the approach in Coq, for example, among other languages.) Does this conflict in any way with typed holes? Perhaps a programmer wants to get an informative error message, not for GHC to plug in a value. 
     73 
     74* Visible, non-dependent arguments cannot be inferred via unification, so `_` would not be applicable here, and would retain its current meaning of a typed hole. 
     75 
     76* How to override an invisible, dependent type argument? This might be critical if a function call would be otherwise ambiguous. (Today's Haskell would benefit from this override occasionally, too. See TypeApplication.) One proposal is that `@` would serve double-duty: it would override invisibility and also indicate a type argument. If this is the case, the `forall (...) ->` form would be essentially useless, as it would still require users to use `@` to indicate parsing. Thus, `forall (...) ->` seems strictly worse than `forall (...) .`. 
     77 
     78* How to override an invisible, dependent term argument (that is, `pi (...) .`)? Using `@` would not work, because the parser wouldn't be able to deal with it. Alternatively, `pi`-bound arguments could use type-level syntax, and then `@` would work. However, this seems suboptimal, as we would more often want to use, say, a data constructor in a `pi`-bound argument, not a type constructor. Braces could possibly work, at least in expressions. These would not conflict with record-update syntax because record-updates require an `=`, but `pi`-bound arguments would not. Patterns might be problematic with braces, because record puns do not require `=`. There are no other proposals here, for the moment. 
    6979 
    7080= Related work = 
     
    7585 
    7686* [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. 
    77 * [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. 
     87* [https://personal.cis.strath.ac.uk/adam.gundry/thesis/thesis-2013-07-24.pdf Type Inference, Haskell, and Dependent Types]. [=#gundry Adam Gundry.] PhD Thesis, 2013. 
    7888 
    7989There are also many works addressing the use of dependent types in Haskell. Here is a selection: 
     
    8191* [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. 
    8292* [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. 
     93* [http://www.cis.upenn.edu/~eir/papers/2014/promotion/promotion.pdf Promoting Functions to Type Families in Haskell]. [=#promotion Richard A. Eisenberg and Jan Stolarek.] Draft, 2014.