Tracking Kinds

Members

• Eelco Lempsink
• Chris Eidhof

Plan

What has to happen? (TODO: update the schedule, it's already outdated)

1. Describe the problem thoroughly (Done: 23 sep)
2. Find and read the literature (Done: 5 oct)
3. Understand in which places we have to modify EHC (Done: 5 oct)
4. Implement it, build testcases (Done: 19 oct)
5. Document it (Done: 26 oct)
6. Write about it / build a presentation. (Done: 1 nov)

Next Actions

• Plan a meeting with Atze to come up with a good description and understanding of the problem
• Understand the regression tests of EHC 6.
• Refresh our understanding of the testcase
• Create a new EHC branch in our own repository
• Let Atze check our goals
• Come up with rules to be added to f-omega for kind polymorphism
• Define kind-erasure on that language
• Try to find more examples, especially where kind polymorphism is actually useful
• Understand where we have to modify EHC
  • Do we need to add rules?
• Extend EHC
  • Give (all) kind annotations
  • Let the user add kind annotations
  • Fix the bugs
• Read up on the references of Pierce I - Chapter 29
• Search for other papers on Type Operators and Kinding
• Create test-cases for all of our goals

Example Problems

let data Min a = Min (forall f . f a) -- forall a . a -> *
    undefined :: forall a . a
    in let 
      weird :: (a -> Min a) -> Min Min
      weird = \g -> g undefined
      in 3

Because of the first 'a' in the type signature of weird, a is of kind "*". Min is of kind "a -> *". Min and a shouldn't unify because of the different kinds. Currently it looks like some checking is done, but once a kind is established, it isn't passed on in the environment. We need to find out where we have to modify EHC to keep track of a kinding context. We then need to use this information when unifying.

let data Min a = Min (forall f . f a) -- forall a . a -> *
    data List a = Cons a
    undefined :: forall a . a
    in let 
      f :: Min a -> a
      weird :: Min List
      in let
        x = f weird
        in 42

The type of x is List. List has kind *->*. All values should have kind *, so EHC errors here.

Goals

• Propagate the kind adminstration properly (map from type variables to kinds, varmp?)
  • Create kind-variables when inferencing types (design choice?)
• Check the kinds in the (type) unification algorithm
• Parse kind annotations in code
• (Note: for polymorphic kinds?)

Reading

@book{509043,
 author = {Benjamin C. Pierce},
 title = {Types and programming languages},
 year = {2002},
 isbn = {0-262-16209-1},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
 }

• Atze's PhD thesis

Links

• Kind Inference (Haskell 98 Report)
• Kind Annotations (Haskell Prime Wiki)
• Explicitly-kinded quantification (GHC Manual)

-- ChrisEidhof - 27 Sep 2007

• handout.pdf: