Re: Concrete syntax for open type kind?

Thanks for that explanation, Simon. The new scheme sounds neater, indeed. Looks like the same trick used for inheritance mentioned in Calling *hell*from *heaven* and *heaven* from *hell*http://research.microsoft.com/pubs/64260/comserve.ps.gz . Meanwhile, I think I can work around the limitation, somewhat clumsily, of no open kinds if I could make a definition polymorphic over unlifted kinds, e.g.,

foo :: # foo = error "foo?"

Is it possible to do so with any sort of concrete syntax? -- Conal On Wed, Apr 16, 2014 at 2:35 PM, Simon Peyton Jones wrote:

Does anyone remember the justification of not having unlifted or open kinds in the source language?

They aren’t in the source language because they are a gross hack, with many messy consequences. Particularly the necessary sub-kinding, and the impact on inference. I’m not proud of it.

But I do have a plan. Namely to use polymorphism. Currently we have

kinds k ::= * | # | ? | k1 -> k2 | ...

Instead I propose

kinds k ::= TYPE bx | k1 -> k2 | ....

boxity bx ::= BOXED | UNBOXED | bv

where bv is a boxity variable

So

· * = TYPE BOXED

· # = TYPE UNBOXED

· ? = TYPE bv

Now error is polymorphic:

error :: forall bv. forall (a:TYPE bv). String -> a

And now everything will work out smoothly I think. And it should be reasonably easy to expose in the source language.

All that said, there’s never enough time to do these things.

Simon

*From:* Glasgow-haskell-users [mailto: glasgow-haskell-users-bounces@haskell.org] *On Behalf Of *Conal Elliott *Sent:* 16 April 2014 18:01 *To:* Richard Eisenberg *Cc:* glasgow-haskell-users@haskell.org *Subject:* Re: Concrete syntax for open type kind?

Oops! I was reading ParserCore.y, instead of Parser.y.pp. Thanks.

Too bad it's not possible to replicate this type interpretation of `error` and `undefined`. I'm doing some Core transformation, and I have a polymorphic function (reify) that I want to apply to expressions of lifted and unlifted types, as a way of structuring the transformation. When my transformation gets to unlifted types, the application violates the *-kindedness of my polymorphic function. I can probably find a way around. Maybe I'll build the kind-incorrect applications and then make sure to transform them away in the end. Currently, the implementation invokes `error`.

Does anyone remember the justification of not having unlifted or open kinds in the source language?

-- Conal

On Tue, Apr 15, 2014 at 5:09 PM, Richard Eisenberg wrote:

What version of the GHC code are you looking at? The parser is currently stored in compiler/parser/Parser.y.pp (note the pp) and doesn’t have these lines. As far as I know, there is no way to refer to OpenKind from source.

You’re absolutely right about the type of `undefined`. `undefined` (and `error`) have magical types. GHC knows that GHC.Err defines an `undefined` symbol and gives it its type by fiat. There is no way (I believe) to reproduce this behavior.

If you have -fprint-explicit-foralls and -fprint-explicit-kinds enabled, quantified variables of kind * are not given kinds in the output. So, the lack of a kind annotation tells you that `a`’s kind is *. Any other kind (assuming these flags) would be printed.

I hope this helps!

Richard

On Apr 15, 2014, at 7:39 PM, Conal Elliott wrote:

I see ‘#’ for unlifted and ‘?’ for open kinds in compiler/parser/Parser.y:

akind :: { IfaceKind }

: '*' { ifaceLiftedTypeKind }

| '#' { ifaceUnliftedTypeKind }

| '?' { ifaceOpenTypeKind }

| '(' kind ')' { $2 }

kind :: { IfaceKind }

: akind { $1 }

| akind '->' kind { ifaceArrow $1 $3 }

However, I don’t know how to get GHC to accept ‘#’ or ‘?’ in a kind annotation. Are these kinds really available to source programs.

I see that undefined has an open-kinded type:

*Main> :i undefined

undefined :: forall (a :: OpenKind). a -- Defined in ‘GHC.Err’

Looking in the GHC.Err source, I just see the following:

undefined :: a

undefined = error "Prelude.undefined"

However, if I try similarly,

q :: a

q = error "q"

I don’t see a similar type:

*X> :i q

q :: forall a. a -- Defined at ../test/X.hs:12:1

I don't know what kind 'a' has here, nor how to find out.

-- Conal

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users