<div dir="ltr"><blockquote>
</blockquote><p>Thanks, Simon. I wouldn’t say that I’m really really stuck yet, and
I’d rather no one wasted time on a dead-end workaround. I like the plan
you described using kind polymorphism instead of subkinding, because I
think the relaxed kinds would naturally be inferred where I need them.</p>
<p>The problem I’m trying to solve here is defining a GADT for
statically typed expressions, where some types are lifted and some are
unlifted:</p>
<pre style="margin-left:40px" class=""><code class=""><span class="">data</span> <span class="">E</span> <span class="">∷</span> <span class="">?</span> <span class="">→</span> <span class="">*</span> <span class="">where</span>
⋯
<span class="">App</span> <span class="">∷</span> <span class="">∀</span> (a <span class="">∷</span> <span class="">?</span>) (b <span class="">∷</span> <span class="">?</span>) <span class="">.</span> <span class="">E</span> (a <span class="">→</span> b) <span class="">→</span> <span class="">E</span> a <span class="">→</span> <span class="">E</span> b
⋯</code></pre>
<p>All literals would be monomorphic and unlifted, and <code>E</code> itself is lifted, so we’d never need to represent anything of an open-kinded type in GHC’s RTS. Instead, the <code>?</code>
kinds here are purely for managing the type constraints needed to
ensure well-typedness of represented expressions while still allowing
enough generality, including both lifted and unlifted types. Without
support for open kinds (somehow), I don’t know of any way to say what I
need to say.</p>
<p>I’ll keep trying to find ways to avoid this limitation. Meanwhile, I’d
like to explore what it’d take to change over the current subkinding
system to the polymorphic one. I’ve not done such a project, but I’d be
glad to help and learn my way around in the process.</p><p>-- Conal<br></p><blockquote>
</blockquote></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Apr 21, 2014 at 12:20 AM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div link="blue" vlink="purple" lang="EN-GB">
<div><div class="">
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12.0pt;margin-left:36.0pt">
Is it possible to do so with any sort of concrete syntax?<u></u><u></u></p>
</div><p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">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?<br>
<br>
S<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US">From:</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US"> Glasgow-haskell-users [mailto:<a href="mailto:glasgow-haskell-users-bounces@haskell.org" target="_blank">glasgow-haskell-users-bounces@haskell.org</a>]
<b>On Behalf Of </b>Conal Elliott<br>
<b>Sent:</b> 19 April 2014 01:11<br>
<b>To:</b> Simon Peyton Jones</span></p><div><div class="h5"><br>
<b>Cc:</b> <a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.org</a><br>
<b>Subject:</b> Re: Concrete syntax for open type kind?<u></u><u></u></div></div><p></p>
</div>
</div><div><div class="h5">
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12.0pt;margin-left:0cm">
Thanks for that explanation, Simon. The new scheme sounds neater, indeed. Looks like the same trick used for inheritance mentioned in
<a href="http://research.microsoft.com/pubs/64260/comserve.ps.gz" target="_blank">Calling <em>hell</em> from
<em>heaven</em> and <em>heaven</em> from <em>hell</em></a>.<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12.0pt;margin-left:0cm">
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.,<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
> foo :: #<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12.0pt;margin-left:0cm">
> foo = error "foo?"<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12.0pt;margin-left:0cm">
Is it possible to do so with any sort of concrete syntax?<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
-- Conal<u></u><u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
</div>
</div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12.0pt;margin-left:0cm">
<u></u> <u></u></p>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
On Wed, Apr 16, 2014 at 2:35 PM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>> wrote:<u></u><u></u></p>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt;margin-left:36.0pt">
Does anyone remember the justification of not having unlifted or open kinds in the source language?<u></u><u></u></p>
</div>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">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.</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">But I do have a plan. Namely to use polymorphism. Currently we have</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> kinds k ::= * | # | ? | k1 -> k2 | ...</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Instead I propose</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> kinds k ::= TYPE bx | k1 -> k2 | ....</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> boxity bx ::= BOXED | UNBOXED | bv</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">where bv is a boxity variable</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">So
</span><u></u><u></u></p>
<p><span style="font-size:11.0pt;font-family:Symbol;color:#1f497d">·</span><span style="font-size:7.0pt;color:#1f497d">
</span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">* = TYPE BOXED</span><u></u><u></u></p>
<p><span style="font-size:11.0pt;font-family:Symbol;color:#1f497d">·</span><span style="font-size:7.0pt;color:#1f497d">
</span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"># = TYPE UNBOXED</span><u></u><u></u></p>
<p><span style="font-size:11.0pt;font-family:Symbol;color:#1f497d">·</span><span style="font-size:7.0pt;color:#1f497d">
</span><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">? = TYPE bv</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Now error is polymorphic:</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> error :: forall bv. forall (a:TYPE bv). String -> a</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">And now everything will work out smoothly I think. And it should be reasonably easy to expose in
the source language.</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">All that said, there’s never enough time to do these things.</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> </span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Simon</span><u></u><u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"> </span><u></u><u></u></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US">From:</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US">
Glasgow-haskell-users [mailto:<a href="mailto:glasgow-haskell-users-bounces@haskell.org" target="_blank">glasgow-haskell-users-bounces@haskell.org</a>]
<b>On Behalf Of </b>Conal Elliott<br>
<b>Sent:</b> 16 April 2014 18:01<br>
<b>To:</b> Richard Eisenberg<br>
<b>Cc:</b> <a href="mailto:glasgow-haskell-users@haskell.org" target="_blank">glasgow-haskell-users@haskell.org</a><br>
<b>Subject:</b> Re: Concrete syntax for open type kind?</span><u></u><u></u></p>
</div>
</div>
<div>
<div>
<p class="MsoNormal"> <u></u><u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt">Oops! I was reading ParserCore.y, instead of Parser.y.pp. Thanks.<br>
<br>
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`.<br>
<br>
Does anyone remember the justification of not having unlifted or open kinds in the source language?<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-bottom:6.0pt">-- Conal<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:12.0pt"> <u></u><u></u></p>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">On Tue, Apr 15, 2014 at 5:09 PM, Richard Eisenberg <<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>> wrote:<u></u><u></u></p>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-top:5.0pt;margin-right:0cm;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">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.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">I hope this helps!<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">Richard<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
<div>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">On Apr 15, 2014, at 7:39 PM, Conal Elliott <<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>> wrote:<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-bottom:6.0pt"> <u></u><u></u></p>
</div>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<div>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:6.0pt">I see ‘#’ for unlifted and ‘?’ for open kinds in compiler/parser/Parser.y:
<u></u><u></u></p>
<pre style="margin-left:30.0pt"><code>akind :: { IfaceKind }</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code> : '*' { ifaceLiftedTypeKind } </code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code> | '#' { ifaceUnliftedTypeKind }</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code> | '?' { ifaceOpenTypeKind }</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code> | '(' kind ')' { $2 }</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code> </code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code>kind :: { IfaceKind }</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code> : akind { $1 }</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code> | akind '->' kind { ifaceArrow $1 $3 }</code><u></u><u></u></pre>
<p>However, I don’t know how to get GHC to accept ‘#’ or ‘?’ in a kind annotation. Are these kinds really available to source programs.<u></u><u></u></p>
<p>I see that undefined has an open-kinded type:<u></u><u></u></p>
<pre style="margin-left:30.0pt"><code>*Main> :i undefined</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code>undefined :: forall (a :: OpenKind). a -- Defined in ‘GHC.Err’</code><u></u><u></u></pre>
<p>Looking in the GHC.Err source, I just see the following:<u></u><u></u></p>
<pre style="margin-left:30.0pt"><code>undefined :: a</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code>undefined = error "Prelude.undefined"</code><u></u><u></u></pre>
<p>However, if I try similarly,<u></u><u></u></p>
<pre style="margin-left:30.0pt"><code>q :: a</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code>q = error "q"</code><u></u><u></u></pre>
<p>I don’t see a similar type:<u></u><u></u></p>
<pre style="margin-left:30.0pt"><code>*X> :i q</code><u></u><u></u></pre>
<pre style="margin-left:30.0pt"><code>q :: forall a. a -- Defined at ../test/X.hs:12:1</code><u></u><u></u></pre>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-bottom:12.0pt">I don't know what kind 'a' has here, nor how to find out.<u></u><u></u></p>
</div>
<p class="MsoNormal">-- Conal<u></u><u></u></p>
</div>
</div>
</div>
<p class="MsoNormal">_______________________________________________<br>
Glasgow-haskell-users mailing list<br>
<a href="mailto:Glasgow-haskell-users@haskell.org" target="_blank">Glasgow-haskell-users@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/glasgow-haskell-users" target="_blank">http://www.haskell.org/mailman/listinfo/glasgow-haskell-users</a><u></u><u></u></p>
</blockquote>
</div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
</blockquote>
</div>
<p class="MsoNormal"> <u></u><u></u></p>
</div>
</div>
</div>
</div>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div></div></div>
</div>
</div>
</blockquote></div><br></div>