Typing Haskell in Haskell experience

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

Typing Haskell in Haskell experience

Christopher Done-2

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 Nat
main = 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.
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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 Nat
main = 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Typing Haskell in Haskell experience

Christopher Done-2
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 <[hidden email]> 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 <[hidden email]> 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 Nat
main = 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 Nat
main = 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net




--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Typing Haskell in Haskell experience

Christopher Done-2
Good points! 

On 3 May 2017 at 20:21, Brandon Allbery <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 <[hidden email]> 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 Nat
main = 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
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net




--
brandon s allbery kf8nh                               sine nomine associates
[hidden email]                                  [hidden email]
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net


_______________________________________________
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.