[Haskell-cafe] Typing Haskell in Haskell experience

[Brandon Allbery]

More that one could argue for two different ways to resolve it: in the
typechecker as you describe, or at link time (that is, we codegen
references to a dictionary and let the linker determine whether said
dictionary exists). Each has drawbacks and advantages.

On Wed, May 3, 2017 at 3:18 PM, Christopher Done <chrisdone at gmail.com>
wrote:

> Are you speculating that THIH probably intentionally leaves how to resolve
> the particular instance for e.g. `Show Bool` as an exercise for the reader,
> instead only implementing that Bool satisfies the shape expected for the
> class head?
>
> On 3 May 2017 at 19:59, Brandon Allbery <allbery.b at gmail.com> wrote:
>
>> Doesn't this more or less mirror the problem with instance visibility
>> that leads to the orphan instance problem?
>>
>> On Wed, May 3, 2017 at 2:46 PM, Christopher Done <chrisdone at gmail.com>
>> wrote:
>>
>>> I’ve been working through Typing Haskell in Haskell in detail (
>>> https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b), and I noticed
>>> that if I change e.g. SourcePrelude.hs from the Hackage package (
>>> http://hackage.haskell.org/package/thih) to have a declaration like
>>> this:
>>>
>>>     [("printZ",
>>>       Just (Forall []
>>>              ([] :=>
>>>               (tString))),
>>>       [([],
>>>         ap [econst showMfun, econst (("Z" :>: toScheme (TCon (Tycon "Nat" Star))))])])],
>>>
>>> In other words
>>>
>>> printChar = show (Z :: Nat)
>>>
>>> Where Z is neither defined nor an instance of Show, it type checks just
>>> fine. If I replace it with e.g. toScheme (TVar(Tyvar "k" Star)) i.e.
>>> “some thing of type k“, then it complains that the instance is
>>> ambiguous, which is true.
>>>
>>> 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.
>>>
>>> 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.
>>>
>>> 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: http://chrisdone.com/toys/duet-gamma/
>>>
>>> You can see the problem illustrated if you type e.g. the following in
>>> the top-left:
>>>
>>> data Nat = Z | S Natmain = show Z
>>>
>>> The type inferred is:
>>>
>>> main = ((show :: (Show Nat) => Nat -> String) (Z :: Nat) :: (Show Nat) => String)
>>>
>>> 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?
>>>
>>> So beware future travelers… THIH is awesome, but these are the things
>>> I’ve found missing.
>>>
>>> Ciao!
>>> ​
>>>
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> To (un)subscribe, modify options or view archives go to:
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>> Only members subscribed via the mailman list are allowed to post.
>>>
>>
>>
>>
>> --
>> brandon s allbery kf8nh                               sine nomine
>> associates
>> allbery.b at gmail.com
>> ballbery at sinenomine.net
>> unix, openafs, kerberos, infrastructure, xmonad
>> http://sinenomine.net
>>
>
>


-- 
brandon s allbery kf8nh                               sine nomine associates
allbery.b at gmail.com                                  ballbery at sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170503/52ece9a2/attachment.html>