<div dir="ltr">Doesn't this more or less mirror the problem with instance visibility that leads to the orphan instance problem?</div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 3, 2017 at 2:46 PM, Christopher Done <span dir="ltr"><<a href="mailto:chrisdone@gmail.com" target="_blank">chrisdone@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="m_-6643315683928402302markdown-here-wrapper"><p style="margin:0px 0px 1.2em!important">I’ve been working through Typing Haskell in Haskell in detail (<a href="https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b" target="_blank">https://gist.github.com/<wbr>chrisdone/0075a16b32bfd4f62b7b</a><wbr>), and I noticed that if I change e.g. SourcePrelude.hs from the Hackage package (<a href="http://hackage.haskell.org/package/thih" target="_blank">http://hackage.haskell.org/<wbr>package/thih</a>) to have a declaration like this:</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code class="m_-6643315683928402302hljs m_-6643315683928402302language-haskell" style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline;white-space:pre-wrap;overflow:auto;border-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important;display:block;overflow-x:auto;padding:0.5em;color:rgb(51,51,51);background:rgb(248,248,248)"> [(<span class="m_-6643315683928402302hljs-string" style="color:rgb(221,17,68)">"printZ"</span>,
<span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Just</span> (<span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Forall</span> []
([] :=>
(tString))),
[([],
ap [econst showMfun, econst ((<span class="m_-6643315683928402302hljs-string" style="color:rgb(221,17,68)">"Z"</span> :>: toScheme (<span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">TCon</span> (<span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Tycon</span> <span class="m_-6643315683928402302hljs-string" style="color:rgb(221,17,68)">"Nat"</span> <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Star</span>))))])])],
</code></pre>
<p style="margin:0px 0px 1.2em!important">In other words</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code class="m_-6643315683928402302hljs m_-6643315683928402302language-haskell" style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline;white-space:pre-wrap;overflow:auto;border-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important;display:block;overflow-x:auto;padding:0.5em;color:rgb(51,51,51);background:rgb(248,248,248)"><span class="m_-6643315683928402302hljs-title" style="color:rgb(153,0,0);font-weight:bold">printChar</span> = show (<span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Z</span> :: <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Nat</span>)
</code></pre>
<p style="margin:0px 0px 1.2em!important">Where Z is neither defined nor an instance of <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline">Show</code>, it type checks just fine. If I replace it with e.g. <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline">toScheme (TVar(Tyvar "k" Star))</code> i.e. “some thing of type <code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline">k</code>“, then it complains that the instance is ambiguous, which is true.</p>
<p style="margin:0px 0px 1.2em!important">So it seems that THIH will accept any type as an instance of any class without complaint as long as all the type variables have been filled in with the correct kind. This came as a surprise to me, as I’m using it in a project. There is apparently code in the type checker that pays attention to the class environment, and you provide instances to it, but it doesn’t seem to care what instances are provided or not.</p>
<p style="margin:0px 0px 1.2em!important">I believe I’ll have to do some extra work to check that the instances actually exist and are full resolved. I can’t tell whether this is a bug or intended behavior. I tried emailing the author of THIH but his email bounced back. Frankly the actual interesting bit of the type checker — the bit where we resolve class instances — is actually the hardest bit for me to read and the bit I’d like more exposition on.</p>
<p style="margin:0px 0px 1.2em!important">I’ve written a tokenizer, parser, renamer and thanks to THIH an inferer, and a stepper in a small dialect of Haskell I’m calling Duet. There’s an example here: <a href="http://chrisdone.com/toys/duet-gamma/" target="_blank">http://chrisdone.com/toys/<wbr>duet-gamma/</a></p>
<p style="margin:0px 0px 1.2em!important">You can see the problem illustrated if you type e.g. the following in the top-left:</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code class="m_-6643315683928402302hljs m_-6643315683928402302language-haskell" style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline;white-space:pre-wrap;overflow:auto;border-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important;display:block;overflow-x:auto;padding:0.5em;color:rgb(51,51,51);background:rgb(248,248,248)"><span class="m_-6643315683928402302hljs-typedef"><span class="m_-6643315683928402302hljs-keyword" style="color:rgb(51,51,51);font-weight:bold">data</span> <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Nat</span> = <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Z</span> | <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">S</span> <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Nat</span></span>
<span class="m_-6643315683928402302hljs-title" style="color:rgb(153,0,0);font-weight:bold">main</span> = show <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Z</span>
</code></pre>
<p style="margin:0px 0px 1.2em!important">The type inferred is:</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code class="m_-6643315683928402302hljs m_-6643315683928402302language-haskell" style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline;white-space:pre-wrap;overflow:auto;border-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important;display:block;overflow-x:auto;padding:0.5em;color:rgb(51,51,51);background:rgb(248,248,248)"><span class="m_-6643315683928402302hljs-title" style="color:rgb(153,0,0);font-weight:bold">main</span> = ((show :: (<span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Show</span> <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Nat</span>) => <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Nat</span> -> <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">String</span>) (<span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Z</span> :: <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Nat</span>) :: (<span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Show</span> <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">Nat</span>) => <span class="m_-6643315683928402302hljs-type" style="color:rgb(68,85,136);font-weight:bold">String</span>)
</code></pre>
<p style="margin:0px 0px 1.2em!important">Which is at least enough information for me to do a lookup and insert an instance dictionary. But I sort of would have expected the type checker to say “no instance”. It does explicitly say that you have to do your own dependency analysis and renamer, but the instance part isn’t clear to me. Oh, and you also have to write your own kind inference for data type declarations. Who knew implementing a Haskell was so involved?</p>
<p style="margin:0px 0px 1.2em!important">So beware future travelers… THIH is awesome, but these are the things I’ve found missing.</p>
<p style="margin:0px 0px 1.2em!important">Ciao!</p>
<div title="MDH:SSd2ZSBiZWVuIHdvcmtpbmcgdGhyb3VnaCBUeXBpbmcgSGFza2VsbCBpbiBIYXNrZWxsIGluIGRl
dGFpbCAoaHR0cHM6Ly9naXN0LmdpdGh1Yi5jb20vY2hyaXNkb25lLzAwNzVhMTZiMzJiZmQ0ZjYy
YjdiKSwgYW5kIEkgbm90aWNlZCB0aGF0IGlmIEkgY2hhbmdlIGUuZy4gU291cmNlUHJlbHVkZS5o
cyBmcm9tIHRoZSBIYWNrYWdlIHBhY2thZ2UgKGh0dHA6Ly9oYWNrYWdlLmhhc2tlbGwub3JnL3Bh
Y2thZ2UvdGhpaCkgdG8gaGF2ZSBhIGRlY2xhcmF0aW9uIGxpa2UgdGhpczo8ZGl2Pjxicj48L2Rp
dj48ZGl2PmBgYCBoYXNrZWxsPC9kaXY+PGRpdj48ZGl2PiZuYnNwOyAmbmJzcDsgWygicHJpbnRa
Iiw8L2Rpdj48ZGl2PiZuYnNwOyAmbmJzcDsgJm5ic3A7IEp1c3QgKEZvcmFsbCBbXTwvZGl2Pjxk
aXY+Jm5ic3A7ICZuYnNwOyAmbmJzcDsgJm5ic3A7ICZuYnNwOyAmbmJzcDsgJm5ic3A7KFtdIDo9
Jmd0OzwvZGl2PjxkaXY+Jm5ic3A7ICZuYnNwOyAmbmJzcDsgJm5ic3A7ICZuYnNwOyAmbmJzcDsg
Jm5ic3A7ICh0U3RyaW5nKSkpLDwvZGl2PjxkaXY+Jm5ic3A7ICZuYnNwOyAmbmJzcDsgWyhbXSw8
L2Rpdj48ZGl2PiZuYnNwOyAmbmJzcDsgJm5ic3A7ICZuYnNwOyBhcCBbZWNvbnN0IHNob3dNZnVu
LCBlY29uc3QgKCgiWiIgOiZndDs6IHRvU2NoZW1lIChUQ29uIChUeWNvbiAiTmF0IiBTdGFyKSkp
KV0pXSldLDwvZGl2PjwvZGl2PjxkaXY+YGBgPC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj5JbiBv
dGhlciB3b3JkczwvZGl2PjxkaXY+PGJyPjwvZGl2PjxkaXY+YGBgIGhhc2tlbGw8L2Rpdj48ZGl2
PnByaW50Q2hhciA9IHNob3cgKFogOjogTmF0KTwvZGl2PjxkaXY+YGBgPC9kaXY+PGRpdj48YnI+
PC9kaXY+PGRpdj5XaGVyZSBaIGlzIG5laXRoZXIgZGVmaW5lZCBub3IgYW4gaW5zdGFuY2Ugb2Yg
YFNob3dgLCBpdCB0eXBlIGNoZWNrcyBqdXN0IGZpbmUuIElmIEkgcmVwbGFjZSBpdCB3aXRoIGUu
Zy4gYHRvU2NoZW1lIChUVmFyKFR5dmFyICJrIiBTdGFyKSlgIGkuZS4gInNvbWUgdGhpbmcgb2Yg
dHlwZSBga2AiLCB0aGVuIGl0IGNvbXBsYWlucyB0aGF0IHRoZSBpbnN0YW5jZSBpcyBhbWJpZ3Vv
dXMsIHdoaWNoIGlzIHRydWUuPC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj5TbyBpdCBzZWVtcyB0
aGF0IFRISUggd2lsbCBhY2NlcHQgYW55IHR5cGUgYXMgYW4gaW5zdGFuY2Ugb2YgYW55IGNsYXNz
IHdpdGhvdXQgY29tcGxhaW50IGFzIGxvbmcgYXMgYWxsIHRoZSB0eXBlIHZhcmlhYmxlcyBoYXZl
IGJlZW4gZmlsbGVkIGluIHdpdGggdGhlIGNvcnJlY3Qga2luZC4gVGhpcyBjYW1lIGFzIGEgc3Vy
cHJpc2UgdG8gbWUsIGFzIEknbSB1c2luZyBpdCBpbiBhIHByb2plY3QuIFRoZXJlIGlzIGFwcGFy
ZW50bHkgY29kZSBpbiB0aGUgdHlwZSBjaGVja2VyIHRoYXQgcGF5cyBhdHRlbnRpb24gdG8gdGhl
IGNsYXNzIGVudmlyb25tZW50LCBhbmQgeW91IHByb3ZpZGUgaW5zdGFuY2VzIHRvIGl0LCBidXQg
aXQgZG9lc24ndCBzZWVtIHRvIGNhcmUgd2hhdCBpbnN0YW5jZXMgYXJlIHByb3ZpZGVkIG9yIG5v
dC48L2Rpdj48ZGl2Pjxicj48L2Rpdj48ZGl2PkkgYmVsaWV2ZSBJJ2xsIGhhdmUgdG8gZG8gc29t
ZSBleHRyYSB3b3JrIHRvIGNoZWNrIHRoYXQgdGhlIGluc3RhbmNlcyBhY3R1YWxseSBleGlzdCBh
bmQgYXJlIGZ1bGwgcmVzb2x2ZWQuIEkgY2FuJ3QgdGVsbCB3aGV0aGVyIHRoaXMgaXMgYSBidWcg
b3IgaW50ZW5kZWQgYmVoYXZpb3IuIEkgdHJpZWQgZW1haWxpbmcgdGhlIGF1dGhvciBvZiBUSElI
IGJ1dCBoaXMgZW1haWwgYm91bmNlZCBiYWNrLiBGcmFua2x5IHRoZSBhY3R1YWwgaW50ZXJlc3Rp
bmcgYml0IG9mIHRoZSB0eXBlIGNoZWNrZXIgLS0gdGhlIGJpdCB3aGVyZSB3ZSByZXNvbHZlIGNs
YXNzIGluc3RhbmNlcyAtLSBpcyBhY3R1YWxseSB0aGUgaGFyZGVzdCBiaXQgZm9yIG1lIHRvIHJl
YWQgYW5kIHRoZSBiaXQgSSdkIGxpa2UgbW9yZSBleHBvc2l0aW9uIG9uLjwvZGl2PjxkaXY+PGJy
PjwvZGl2PjxkaXY+SSd2ZSB3cml0dGVuIGEgdG9rZW5pemVyLCBwYXJzZXIsIHJlbmFtZXIgYW5k
IHRoYW5rcyB0byBUSElIIGFuIGluZmVyZXIsIGFuZCBhIHN0ZXBwZXIgaW4gYSBzbWFsbCBkaWFs
ZWN0IG9mIEhhc2tlbGwgSSdtIGNhbGxpbmcgRHVldC4gVGhlcmUncyBhbiBleGFtcGxlIGhlcmU6
Jm5ic3A7aHR0cDovL2NocmlzZG9uZS5jb20vdG95cy9kdWV0LWdhbW1hLzwvZGl2PjxkaXY+PGJy
PjwvZGl2PjxkaXY+WW91IGNhbiBzZWUgdGhlIHByb2JsZW0gaWxsdXN0cmF0ZWQgaWYgeW91IHR5
cGUgZS5nLiB0aGUgZm9sbG93aW5nIGluIHRoZSB0b3AtbGVmdDo8L2Rpdj48ZGl2Pjxicj48L2Rp
dj48ZGl2PmBgYCBoYXNrZWxsPC9kaXY+PGRpdj48ZGl2PmRhdGEgTmF0ID0gWiB8IFMgTmF0PC9k
aXY+PGRpdj5tYWluID0gc2hvdyBaPC9kaXY+PC9kaXY+PGRpdj5gYGA8L2Rpdj48ZGl2Pjxicj48
L2Rpdj48ZGl2PlRoZSB0eXBlIGluZmVycmVkIGlzOjwvZGl2PjxkaXY+PGJyPjwvZGl2PjxkaXY+
YGBgIGhhc2tlbGw8L2Rpdj48ZGl2PjxkaXY+bWFpbiA9ICgoc2hvdyA6OiAoU2hvdyBOYXQpID0m
Z3Q7IE5hdCAtJmd0OyBTdHJpbmcpIChaIDo6IE5hdCkgOjogKFNob3cgTmF0KSA9Jmd0OyBTdHJp
bmcpPC9kaXY+PC9kaXY+PGRpdj5gYGA8L2Rpdj48ZGl2Pjxicj48L2Rpdj48ZGl2PldoaWNoIGlz
IGF0IGxlYXN0IGVub3VnaCBpbmZvcm1hdGlvbiBmb3IgbWUgdG8gZG8gYSBsb29rdXAgYW5kIGlu
c2VydCBhbiBpbnN0YW5jZSBkaWN0aW9uYXJ5LiBCdXQgSSBzb3J0IG9mIHdvdWxkIGhhdmUgZXhw
ZWN0ZWQgdGhlIHR5cGUgY2hlY2tlciB0byBzYXkgIm5vIGluc3RhbmNlIi4gSXQgZG9lcyBleHBs
aWNpdGx5IHNheSB0aGF0IHlvdSBoYXZlIHRvIGRvIHlvdXIgb3duIGRlcGVuZGVuY3kgYW5hbHlz
aXMgYW5kIHJlbmFtZXIsIGJ1dCB0aGUgaW5zdGFuY2UgcGFydCBpc24ndCBjbGVhciB0byBtZS4g
T2gsIGFuZCB5b3UgYWxzbyBoYXZlIHRvIHdyaXRlIHlvdXIgb3duIGtpbmQgaW5mZXJlbmNlIGZv
ciBkYXRhIHR5cGUgZGVjbGFyYXRpb25zLiBXaG8ga25ldyBpbXBsZW1lbnRpbmcgYSBIYXNrZWxs
IHdhcyBzbyBpbnZvbHZlZD88L2Rpdj48ZGl2Pjxicj48L2Rpdj48ZGl2PlNvIGJld2FyZSBmdXR1
cmUgdHJhdmVsZXJzLi4uIFRISUggaXMgYXdlc29tZSwgYnV0IHRoZXNlIGFyZSB0aGUgdGhpbmdz
IEkndmUgZm91bmQgbWlzc2luZy48L2Rpdj48ZGl2Pjxicj48L2Rpdj48ZGl2PkNpYW88L2Rpdj4=" style="height:0;width:0;max-height:0;max-width:0;overflow:hidden;font-size:0em;padding:0;margin:0"></div></div></div>
<br>______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/haskell-<wbr>cafe</a><br>
Only members subscribed via the mailman list are allowed to post.<br></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div>brandon s allbery kf8nh sine nomine associates</div><div><a href="mailto:allbery.b@gmail.com" target="_blank">allbery.b@gmail.com</a> <a href="mailto:ballbery@sinenomine.net" target="_blank">ballbery@sinenomine.net</a></div><div>unix, openafs, kerberos, infrastructure, xmonad <a href="http://sinenomine.net" target="_blank">http://sinenomine.net</a></div></div></div>
</div>