Changes between Version 4 and Version 5 of DependentHaskell

May 27, 2014 12:45:20 PM (3 years ago)



  • DependentHaskell

    v4 v5  
    1111As 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.
    13 Haskell currently has two quantifiers: `forall` and `->`, as classified in the following table:
     13Haskell currently has three quantifiers: `forall`, `->`, and `=>`, as classified in the following table:
    15 ||= Quantifier =||= Dependent? =||= Visible? =||= Relevant? =||
    16 || `forall` || yes || no || no ||
    17 || `->` || no || yes || yes ||
     15||= Quantifier =||= Dependent? =||= Visible? =||= Required? =||= Relevant? =||
     16|| `forall` || yes || unification || FVs || no ||
     17|| `->` || no || yes || yes || yes ||
     18|| `=>` || no || solving || yes || yes ||
     20* ''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 `->`!)
     21* ''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.
     22* 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).
     23* ''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.
     24Relevance 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.
    1928== Related work ==