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-boun...@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
<e...@cis.upenn.edu<mailto:e...@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
<co...@conal.net<mailto:co...@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@haskell.org<mailto:Glasgow-haskell-users@haskell.org>
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
