[Haskell-cafe] Typing Haskell in Haskell experience

[Christopher Done]

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