Changes between Version 16 and Version 17 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 4:58:15 PM (11 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v16 v17  
    2525||||||||||  Current Haskell  || 
    2626||= Quantifier =||= Dependent? =||= Visible? =||= Required? =||= Relevant? =|| 
    27 || `forall` || yes || No (unification) || No (FVs) || No || 
    28 || `->` || no || Yes (as term) || Yes || Yes || 
    29 || `=>` || no || No (solving) || Yes || Yes || 
     27|| `forall` || Yes || No (unification) || No (FVs) || No || 
     28|| `->` || No || Yes (as term) || Yes || Yes || 
     29|| `=>` || No || No (solving) || Yes || Yes || 
    3030 
    3131 Dependent:: 
     
    4242||||||||||  Dependent Haskell  || 
    4343||= Quantifier =||= Dependent? =||= Visible? =||= Required? =||= Relevant? =|| 
    44 || `forall (...) .` || yes || unification || FVs + Rel.I. || no || 
    45 || `forall (...) ->` || yes || as type || yes || no || 
    46 || `pi (...) .` || yes || unification || FVs + Rel.I. || yes || 
    47 || `pi (...) ->` || yes || as term || yes || yes || 
    48 || `->` || no || as term || yes || yes || 
    49 || `=>` || no || solving || yes || yes || 
     44|| `forall (...) .` || Yes || No (unification) || No (FVs + Rel.I.) || No || 
     45|| `forall (...) ->` || Yes || Yes (as type) || Yes || No || 
     46|| `pi (...) .` || Yes || No (unification) || No (FVs + Rel.I.) || Yes || 
     47|| `pi (...) ->` || Yes || Yes (as term) || Yes || Yes || 
     48|| `->` || No || Yes (as term) || Yes || Yes || 
     49|| `=>` || No || No (solving) || Yes || Yes || 
    5050 
    5151Note 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''.)