[Haskell-cafe] Typing Haskell in Haskell experience

[Brandon Allbery]

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