Concrete syntax for open type kind?

[Simon Peyton Jones]

Is it possible to do so with any sort of concrete syntax?
I’m afraid not.  And I’m strongly disinclined to add it because we’d then just delete it again.  Are you really really stuck?

S

From: Glasgow-haskell-users [mailto:glasgow-haskell-users-bounces at haskell.org] On Behalf Of Conal Elliott
Sent: 19 April 2014 01:11
To: Simon Peyton Jones
Cc: glasgow-haskell-users at haskell.org
Subject: 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 <simonpj at microsoft.com<mailto:simonpj at microsoft.com>> 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 at haskell.org<mailto:glasgow-haskell-users-bounces at haskell.org>] On Behalf Of Conal Elliott
Sent: 16 April 2014 18:01
To: Richard Eisenberg
Cc: glasgow-haskell-users at haskell.org<mailto:glasgow-haskell-users at 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 <eir at cis.upenn.edu<mailto:eir at cis.upenn.edu>> 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 <conal at conal.net<mailto:conal at conal.net>> 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 at haskell.org<mailto:Glasgow-haskell-users at haskell.org>
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140421/a3bc7517/attachment-0001.html>