[Haskell-cafe] Typing Haskell in Haskell experience

[Christopher Done]

Good points!

On 3 May 2017 at 20:21, Brandon Allbery <allbery.b at gmail.com> wrote:

> 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/e6c3299e/attachment.html>