[Haskell-cafe] Typing Haskell in Haskell experience

[Christopher Done]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170503/6465867a/attachment-0001.html>