Changes between Version 22 and Version 23 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 5:59:33 PM (12 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • DependentHaskell

    v22 v23  
    137137* We must have a concrete syntax to declare both of these sorts of type and data families. There are no current proposals for this. 
    138138 
     139= Type Inference = 
     140 
     141Figuring out type inference for this language is a bit of a challenge. While the full design won't be laid out here, interesting tidbits will be gathered here for easy retrieval. 
     142 
     143=== Inferring `pi` types === 
     144 
     145Suppose a programmer writes, without a type signature 
     146 
     147{{{ 
     148foo @Zero y = y 
     149}}} 
     150 
     151(Here, we are assuming `@` as the invisible-overrider.) What is `foo`'s type? It could be `pi (n :: Nat). forall (a :: *). Vec a n -> Vec a Zero`. It could also be `forall (n :: Nat) (a :: *). a -> a`. Neither is more general than the other -- we are in the same GADT type-inference problem as described in the [http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf OutsideIn] paper. Thus, we reject such a `foo` that matches on an implicit parameter without a type signature. 
     152 
     153But, what about 
     154{{{ 
     155foo Zero y = y 
     156}}} 
     157 
     158We are actually in the same situation here. But, backward compatibility compels us to prefer non-dependent types over dependent ones, inferring `foo :: forall (a :: *). Nat -> a -> a`. (Note that `foo :: forall (a :: *). pi (n :: Nat) -> Vec a n -> Vec a Zero` is a valid but incomparable type that we could assign.) 
     159 
     160When do `pi`-types get inferred, if ever? Good question. 
     161 
     162= Implementation = 
     163 
     164The implementation of this is under way, [https://github.com/goldfirere/ghc/tree/nokinds here]. More notes will be added to this section in due course. 
     165 
    139166= Related work = 
    140167