Changes between Version 11 and Version 12 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 2:43:56 PM (14 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v11 v12  
    7070  Thus, we would want to distinguish `pi k. k -> k` (the kind of `F`) and `forall k. k -> k` (the kind of a type-level polymorphic identity). This distinction does not affect erasure or phase, but it does affect how a quantifiee can be used. Furthermore, this keeps term classifiers more in line with type classifiers.
    7171
     72 Datatypes::
     73  How is the kind of a datatype classified? (stub)
     74
    7275== Open design questions ==
    7376
     
    105108* 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.
    106109
     110=== Parametric vs. Non-parametric type families ===
     111
     112* Concrete syntax? (stub)
     113
    107114= Related work =
    108115