You are here: UUCS>TS Web>StudentProjects>TrackingKinds (27 Nov 2007, UnknownUser)

# 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},
}
```

# Links

-- ChrisEidhof - 27 Sep 2007

Topic attachments
I Attachment Action Size Date Who Comment
pdf handout.pdf manage 146.1 K 06 Nov 2007 - 11:48 UnknownUser
pdf presentation.pdf manage 120.5 K 04 Oct 2007 - 09:20 UnknownUser
Topic revision: r18 - 27 Nov 2007, UnknownUser

Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS? Send feedback