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 <simo...@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-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> > 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> 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 > > > > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users