Changes between Version 22 and Version 23 of DependentHaskell


Ignore:
Timestamp:
May 27, 2014 5:59:33 PM (15 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