Concrete syntax for open type kind?

[Conal Elliott]

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>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> 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
> 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/20140416/677653d1/attachment.html>