On 3/18/08, John Meacham <john@repetae.net> wrote:

On Tue, Mar 18, 2008 at 06:09:22PM -0400, Samuel Bronson wrote:

...

I don't understand how FrontEnd.KindInfer.constrain is supposed to deal with KindSimple constraints... it doesn't seem to have any way of replacing ?? or ? with *. Why not?

that is done in the FrontEnd.Tc.Kind.kindCombine routine. The kind inference algorithm is based on the impredicative boxy type inferencer used as the main typechecker. this is because jhc is going to be a kind-polymorphic system, much like the Omega language (based on haskell). That and I find the impredicative boxy typechecking algorithm quite elegant. And when my moratorium on adding new features ends, I want to finish support for bang kinds. so,

data List a = Cons a (List a) | Nil

will actualy declary a type of

List :: forall (k1::**) (k2::**) . \(a::k2) -> k1

(** is the supersort of boxed (but not necessarily lazy) values.

this means you can have

List * * - lazy list of lazy elements List ! * - strict list of lazy elements List * ! - lazy list of strict elements List ! ! - strict list of strict elements

So what is KindInfer.constrain for, then?

On 3/18/08, John Meacham <john@repetae.net> wrote:

'constrain' refines a type subject to constraints, kindCombine actually returns what the unification of the kinds are. constrain works on constraints, combine works on kinds. constraints don't necessarily map to kinds, though currently most have an analog.

Eh? Doesn't KindInfer run before typechecking begins?

On 3/18/08, John Meacham <john@repetae.net> wrote:

On Tue, Mar 18, 2008 at 06:52:04PM -0400, Samuel Bronson wrote:

...

On 3/18/08, John Meacham <john@repetae.net> wrote:

...

'constrain' refines a type subject to constraints, kindCombine actually returns what the unification of the kinds are. constrain works on constraints, combine works on kinds. constraints don't necessarily map to kinds, though currently most have an analog.

Eh? Doesn't KindInfer run before typechecking begins?

excuse me, I meant 'kind', not 'type'. this terminology is real trickylike... At least I made sure that jhc core's axioms allowed a stratified type system so 'term','type','kind','superkind' all are distinct sets and have no cyclic dependencies... though, I am not sure if there are practical languages where that is not the case.. though wacky type systems are fun to play with.

Well, it seems like constrain doesn't really have any choice but to throw an error when asked to constrain a KBase KQuest with a KindSimple constraint... it has no way of indicating that the result should be a KBase KStar!

On Wed, Mar 19, 2008 at 06:21:45PM -0400, Samuel Bronson wrote:

On 3/18/08, Samuel Bronson <naesten@gmail.com> wrote:

...

On 3/18/08, John Meacham <john@repetae.net> wrote:

...

On Tue, Mar 18, 2008 at 06:52:04PM -0400, Samuel Bronson wrote:

...

On 3/18/08, John Meacham <john@repetae.net> wrote:

...

'constrain' refines a type subject to constraints, kindCombine actually returns what the unification of the kinds are. constrain works on constraints, combine works on kinds. constraints don't necessarily map to kinds, though currently most have an analog.

Eh? Doesn't KindInfer run before typechecking begins?

excuse me, I meant 'kind', not 'type'. this terminology is real trickylike... At least I made sure that jhc core's axioms allowed a stratified type system so 'term','type','kind','superkind' all are distinct sets and have no cyclic dependencies... though, I am not sure if there are practical languages where that is not the case.. though wacky type systems are fun to play with.

Well, it seems like constrain doesn't really have any choice but to throw an error when asked to constrain a KBase KQuest with a KindSimple constraint... it has no way of indicating that the result should be a KBase KStar!

I was hoping you might have something to say about this?

Ah, sorry. I was mulling it over. Basically, it has to do with the issue that '?' and '??' are not real kinds. they are just shorthand for kind abstractions. when you say: data App :: ?? -> ? -> * you actually mean: (in psuedo-haskell) data App :: forall (k1 | k1 `elem` [*,#]) (k2 | k2 `elem` [*,#,(#)]) . k1 -> k2 -> * the constraints are what is to the right of the |'s there. (I could also do this with superkinds, though I think constrained polymorphism is the way to go here.). so, ? should not actually be a kind of type '?' but actually a newly instantiated kind variable with a KindQuest constraint on it. This instantiation should be done whenever we pull something out of the kind environment. However, since full kind polymorphism isn't availibe in the front end, we use ? and ?? as placeholders in our code as well as data structures. they actually behave the same as if they had been declared: kindsynonym ?? = exists k | k `elem` [*,#] . k Right now, for compatability with haskell 98 and because I would need to modify some data structures to handle it, we perform a 'defaulting', defaulting all kindvars to * at the end of inference. we could just as easily perform a generalization there and get true kind polymorphism. (and this will be done eventually) note that type synonyms are already kind polymorphic: type UIO a = World__ -> (# World__, a #) 'UIO Int' and 'UIO Bits32_' are both fine. UIO :: forall k . k -> * (actually, to be fully formal, UIO has superkind polymorhism, but that is irrelevant since type synonyms don't make it to jhc core, jhc can handle that fine, but I think I will wait until 'kind level' programming becomes popular before crossing that bridge :) ) so. to answer the question of why that case dealing with KQuest isn't in constrain, it is either because 1. I forgot it, it actually should be there. or 2. an actual '?' or '??' is sneaking in as a kind when it should have been turned into a freshly instantiated kind variable with a ? or ?? constraint as appropriate. as an aside, it is interesting to note that methodless type classes give a sort of constrained polymorphism at the type level, I am not sure the signifigance exactly of this, but it might lead to a more elegant handling of kinds in the future... uncharted waters. John -- John Meacham - ⑆repetae.net⑆john⑈

On Wed, Mar 19, 2008 at 06:55:29PM -0400, Samuel Bronson wrote:

...

2. an actual '?' or '??' is sneaking in as a kind when it should have been turned into a freshly instantiated kind variable with a ? or ?? constraint as appropriate.

Where is this process supposed to happen? I didn't see anything that looked like that in KindInfer, and I don't think it could be anywhere else, since the monad it would need to work in is only available in that module...

Well, that's the thing, I never implemented users being able to use '?' and '??' directly, so I never needed to implement it for user defined kinds. where it currently happens is in KindInfer in all the calls to 'newKindVar' in kiType. notice that when you have an unboxed tuple for instance, its subkinds are declared with ?? constraints. likewise for a function call and so forth. so what needs to happen for user defined ones to work is for 'lookupKind' to create a freshly instantiated version of the constructor with no literal ? or ??'s in it, just constrained kindvars. note that this brings up intruging possibilities. like data Complex (a :: ??) = a :+: a notice you can now have data structures with polymorphic unboxed values in them! so your complex Float can actually have two unboxed floats next to each other. but this raises several other issues when it comes to actaully generating code for that. note also that the primitive pre-defined tArrow in DataConstructors has the wrong type. this is a known bug but the current workarounds are okay for now and it will be a fairly complicated one to fix. John -- John Meacham - ⑆repetae.net⑆john⑈

On Wed, Mar 19, 2008 at 07:16:16PM -0400, Samuel Bronson wrote:

On 3/19/08, John Meacham <john@repetae.net> wrote:

...

On Wed, Mar 19, 2008 at 06:55:29PM -0400, Samuel Bronson wrote:

...

...

2. an actual '?' or '??' is sneaking in as a kind when it should have been turned into a freshly instantiated kind variable with a ? or ?? constraint as appropriate.

Where is this process supposed to happen? I didn't see anything that looked like that in KindInfer, and I don't think it could be anywhere else, since the monad it would need to work in is only available in that module...

Well, that's the thing, I never implemented users being able to use '?' and '??' directly, so I never needed to implement it for user defined kinds.

Well, what are the KBase constructors for, then? "Future proofing" is clearly not a very good answer...

Oh, it is a direct analogy to a 'type scheme' in the type level typechecker. A kind can be either a 'kind' or a 'kind scheme' a 'kind scheme' is something you must instantiate to get a 'kind', just like 'forall a . a -> a' is not a type[1], but rather a type scheme. an actual type it can be instantiated to would be 'Int -> Int' or 'v1 -> v1' (where v1 is a type variable). now, I could extend the 'Kind' type to actually have the full quantification, but since the polymorphism allowed is always of a specific variety, it is easier and more straightforward to just have KQuest and KQuestQuest as placeholders. and Future Proofing is always a good answer, assuming one can back it up, full kind polymorphism is an eventual goal and the kind inference algorithm and terminology used was written with that in mind. oddly enough it leads to a much cleaner implementation than the THIH implementation as a side effect... oh, also note that for all _infered_ kinds, due to defaulting, the kind scheme and the kind will be identical, but the distinction is quite important. [1]. we are ignoring rank 2 polymorphism for now, it doesn't complicate things really from an algorithmic point of view, but it would complicate the discussion and isn't relevant to kinds anyway. John -- John Meacham - ⑆repetae.net⑆john⑈

On Wed, Mar 19, 2008 at 07:37:55PM -0400, Samuel Bronson wrote:

...

and Future Proofing is always a good answer, assuming one can back it up, full kind polymorphism is an eventual goal and the kind inference algorithm and terminology used was written with that in mind. oddly enough it leads to a much cleaner implementation than the THIH implementation as a side effect...

It's only a good answer if the code actually works... dead code doesn't get much testing, generally...

Hrm? I am not sure what you mean. I knew I needed a constrained polymorphic inference algorithm so thats what I wrote. The difference between kind schemes and kinds may not have been obvious because ghc uses a similar (but distinct algorithmically) subtyping algorithm. you might as well complain about someone writing fst3 (x,_,_) = x without explicitly saying fst3 :: (Int,Char,Foo) -> Int because that happens to be the way it is used. one of the most beautiful things about haskell is that the general solution is almost always _easier_ than just solving a specific problem. you gotta work harder to constraint 'fst3', and having to throw away my kindchecker just because I introduced kind schemes would have been a whole lot more work (especially since I knew I was going to introduce them). jhc couldn't exist if I didn't think about the future of every bit of code I write. Luckily, haskell is such a great language, it's hard to write code that isn't future safe, but I'm not gonna go out of my way to work myself into a corner. John -- John Meacham - ⑆repetae.net⑆john⑈