Commutativity question

[paulyoung]

I’m attempting to port some Haskell to PureScript:

-- Haskell
commute :: Foo (a, b) (b, a)
commute = Foo f f where
  f (a, b) = Just (b, a)

-- PureScript
commute :: forall a b. Foo (Tuple a b) (Tuple b a)
commute = Foo f f
  where
  f (Tuple a b) = Just (Tuple b a)

where

data Foo a b = Foo (a -> Maybe b) (b -> Maybe a)

I’m getting this type error:

  Could not match type

    a0

  with type

    b1


while trying to match type Tuple t2 t2
  with type Tuple a0 b1
while checking that expression (Foo f) f
  has type Foo (Tuple a0 b1) (Tuple b1 a0)
in value declaration commute

where b1 is a rigid type variable
        bound at line 28, column 11 - line 30, column 35
      a0 is a rigid type variable
        bound at line 28, column 11 - line 30, column 35
      t2 is an unknown type

If I remove the type signature, the inferred type is:

commute :: forall a. Foo (Tuple a a) (Tuple a a)

I’m uncertain as to whether the inferred type is sufficient, and why this doesn’t work if not.

[paulyoung]

This appears to work:

-- PureScript
commute :: forall a b. Foo (Tuple a b) (Tuple b a)
commute = Foo f g
  where
  f (Tuple a b) = Just (Tuple b a)
  g (Tuple b a) = Just (Tuple a b)

[hdgarrood]

I think the compiler is inferring an overly specific type for your f - I think what’s happening is that it looks at the first occurrence of f in the body of the function, and infers a type using the bound type variables a and b, instead of introducing some new universally quantified type variables, which I think you wanted/expected. If you provide a type signature like f :: forall c d. Tuple c d -> ... does it work?

[natefaubion]

I think @hdgarrood is right. To elaborate, Haskell98 does let generalization. That is it will replace unknowns in a let declaration with foralls while inferring. That means it will infer the most polymorphic function it can. PureScript (and Haskell with various extensions turned on like TypeFamilies and GADTs) does not perform let generalization. So for the first example to work, you have to add the foralls yourself.

For some motivation: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tldi10-vytiniotis.pdf

[coot]

Indeed; adding a type signature will solve the problem:

commute :: forall a b. Foo (Tuple a b) (Tuple b a)
commute = Foo f f
  where
  f :: forall x y. Tuple x y -> Maybe (Tuple y x)
  f (Tuple a b) = Just (Tuple b a)

[paulyoung]

Thanks everyone. Good to know why.