Concrete syntax for open type kind?

[Conal Elliott]

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>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] *On Behalf Of *Conal Elliott
> *Sent:* 16 April 2014 18:01
> *To:* Richard Eisenberg
> *Cc:* 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>
> 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/20140418/49d9b3cb/attachment.html>