Changes between Version 3 and Version 4 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 12:32:01 PM (13 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v3 v4  
    99=== Quantifiers === 
    1010 
    11 As pointed out in the [#hasochism Hasochism paper],  
     11As 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. 
     12 
     13Haskell currently has two quantifiers: `forall` and `->`, as classified in the following table: 
     14 
     15||= Quantifier =||= Dependent? =||= Visible? =||= Relevant? =|| 
     16|| `forall` || yes || no || no || 
     17|| `->` || no || yes || yes || 
    1218 
    1319== Related work ==