[Haskell] Higher kind type inference paper

2006-12-07 Thread Edsko de Vries 
Hi,

Are there any papers that describe how higher kind type inference (and I
really mean higher kind, not higher rank) is done?

Thanks,

Edsko
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Higher kind type inference paper

2006-12-07 Thread Stefan Holdermans 

Edsko,

Are there any papers that describe how higher kind type inference  
(and I

really mean higher kind, not higher rank) is done?


I'm not aware of any specific papers (but maybe someone else can jump  
in, here?), but as long as your kind language is simple enough, say


  k, v ::= *
|  k - v ,

you can apply the well-known techniques from type inference. Assuming  
your kind system does not incorporate kind polymorphism, you could  
just replace generalization by defaulting; so, instead of, for instance


  gen((a - *) - a - b - *) = forall k v. (k - *) - k - v - * ,

you get

  def((a - *) - a - b - *) = (* - *) - * - * - * .

HTH,

  Stefan
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Higher kind type inference paper

2006-12-07 Thread John Meacham 
jhc does it via the simple unification type inference algorithm,
modified to push explicitly given kinds down into terms. so, pretty much
exactly the boxy type inference algorithm, where your kind inference
function looks somewhat like

 data Kind = 
 Star 
 | Fun Kind Kind 
 | Hash
 | UnboxedTuple  -- (#)
 | KVar Constraints (IORef (Maybe Kind))

 data Constraints = 
 AnyKind 
 | SimpleKind  -- * or simplekind - simplekind
 | FunResult   -- ?  * # or (#)
 | Argument-- ?? * or #


 tiKind :: Term - Kind - Ki ()
 tiKind = ...


constraints are how the simple kind subtyping is done. like the rule for
application would be:

 tiKind (TArrow a b) Star = do
 va - newVar FunArg-- ??
 vr - newVar FunResult -- ?
 tiKind a va
 tiKind b vr 

note that ?? and ? arn't real kinds, they are just constraints placed on
what valid kinds can be infered in a given spot. whenever a KVar is
filled in, it is first checked against the constraint, whenever two
KVars are unified, the glb of their constraints is used.

then once everything is done. I unify all free kind variables  with *.

The algorithm is heavily influenced by the 'boxy kind inference paper'
of SPJs. 

the code is in FrontEnd.Tc.Kind and FrontEnd.KindInfer, but it is pretty
hairy, due to it evolving incrementally from my previous algorithm which
envolved from the original hatchet code, which is derived from the THIH
paper.

John


-- 
John Meacham - ⑆repetae.net⑆john⑈
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell