Changes between Version 22 and Version 23 of DependentHaskell

May 27, 2014 5:59:33 PM (11 months ago)



  • 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. 
     139= Type Inference = 
     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. 
     143=== Inferring `pi` types === 
     145Suppose a programmer writes, without a type signature 
     148foo @Zero y = y 
     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 [ OutsideIn] paper. Thus, we reject such a `foo` that matches on an implicit parameter without a type signature. 
     153But, what about 
     155foo Zero y = y 
     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.) 
     160When do `pi`-types get inferred, if ever? Good question. 
     162= Implementation = 
     164The implementation of this is under way, [ here]. More notes will be added to this section in due course. 
    139166= Related work =