Rank N Polymorphism / unification issue

[johnpmayer]

This is a neat one I think; consider the following module:

module Rec where

type Ext a = { a | x : Int }

data Foo = Bar (Ext { y : Int })
         | Baz (Ext { z : Int })

mapExtFoo : (Ext a -> Ext a) -> Foo -> Foo
mapExtFoo f foo = case foo of
  Bar bar -> Bar <| f bar
  Baz baz -> Baz <| f baz

As both "branches" of the Foo data structure contain things that are Ext, if we have a function that maps Ext to Ext, we should be able to apply it independently to both sides, and thus apply it to Foo as a whole.

I think the issue here is that the f argument wants to unify to two different types, but notice that it can uniquely unify within the scope of each case branch. Compiler output below:

[1 of 1] Compiling Rec                 ( Rec.elm )
Type error on line 12:
Something weird is happening with this value:

        baz

   Expected Type: {a | z : Int}
     Actual Type: {}


Type error on line 12:
Something weird is happening with this value:

        baz

   Expected Type: {}
     Actual Type: {a | y : Int}


Type error on line 12:
Something weird is happening with this value:

        Baz <| (f baz)

   Expected Type: {a | z : Int}
     Actual Type: {}


Type error on line 12:
Something weird is happening with this value:

        Baz <| (f baz)

   Expected Type: {}
     Actual Type: {a | y : Int}


Type error between lines 10 and 12:
Cannot unify rigid type variable 'a'.
It is likely that a type annotation is not general enough.

        case foo of
          Bar bar -> Bar <| (f bar)
          Baz baz -> Baz <| (f baz)

   Expected Type: a
     Actual Type: {y : Int}


Type error between lines 10 and 12:
Cannot unify rigid type variable 'a'.
It is likely that a type annotation is not general enough.

        case foo of
          Bar bar -> Bar <| (f bar)
          Baz baz -> Baz <| (f baz)

   Expected Type: a
     Actual Type: {y : Int}

[johnpmayer]

Note that it still fails when I remove the type annotation; it just doesn't print those last two errors.

[johnpmayer]

Huh, this is actually interesting - the following code does not compile in Haskell

foo :: (a -> a) -> (b,c) -> (b,c)
foo f (x,y) = (f x, f y)

[johnpmayer]

Narrowed it down! So it looks like Elm would need to support Rank-2 types for this to work. I'll do some research. Can we keep this open, but tabled?

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

module Dispatch where

foo :: (∀ a. a -> a) -> (b,c) -> (b,c)
foo f (x,y) = (f x, f y)

bar = foo id

[johnpmayer]

For reference: http://ghc.haskell.org/trac/haskell-prime/wiki/Rank2Types

And implementation: http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/putting.pdf

[evancz]

Sorry for the slow response! Yeah, we can definitely keep this open. My intuition was that a forall was needed, so it looks like we agree :)

mapExtFoo : (forall a. Ext a -> Ext a) -> Foo -> Foo

I think the type checker is able to handle this kind of thing, but these types are not parsed at the moment. I feel like this is the kind of thing that might make things undecidable or at least really expensive, but I am not expert enough to know decisively.

[johnpmayer]

According to TAPL, rank 2 is decidable, otherwise rank-n is not.

Sent from my iPhone

On Sep 5, 2013, at 9:22 PM, Evan Czaplicki notifications@github.com wrote:

Sorry for the slow response! Yeah, we can definitely keep this open. My intuition was that a forall was needed, so it looks like we agree :)

mapExtFoo : (forall a. Ext a -> Ext a) -> Foo -> Foo
I think the type checker is able to handle this kind of thing, but these types are not parsed at the moment. I feel like this is the kind of thing that might make things undecidable or at least really expensive, but I am not expert enough to know decisively.

—
Reply to this email directly or view it on GitHub.

[evancz]

Why is it a flag in Haskell then? Maybe it has bad interactions with type classes?

[pthariensflame]

@evancz It's a flag for the same reason DoAndIfThenElse is a flag: because some people want strict adherence to the Haskell standard(s).

[evancz]

Ah, makes sense. Thanks @pthariensflame :)

[evancz]

I'm doing this thing where I make meta issues to track a category of related ideas. In this case, I added this to #1039. Often we have a bunch of different threads open that are mutually exclusive, or depend on each other in tricky ways. This is described more here in the "design discussion" section.

So I am going to close this, but any discussion should continue here!