1

So, I am attempting to develop a function that expects a polymorphic function.

I start with and create a class Foo, to represent the constrained type argument in the example function.

module Test
where

class Foo a

Along with a random type for this example...

newtype Bar = Bar Int

In order to pass Bar to anything that has a Foo constraint, it needs to have a typeclass, so I do so:

instance fooBar :: Foo Bar

Everything should be perfectly fine, however, this doesn't work, psc doesn't think the types unify and I don't know why:

example :: forall a. (Foo a) => (a -> Int) -> Int
example a = a (Bar 42)

Error as follows:

Error found:
in module Test
at /Users/arahael/dev/foreign/test.purs line 11, column 16 - line 11, column 22

  Could not match type

    Bar

  with type

    a0


while checking that type Bar
  is at least as general as type a0
while checking that expression Bar 42
  has type a0
in value declaration example

where a0 is a rigid type variable
        bound at line 11, column 1 - line 11, column 22

See https://github.com/purescript/documentation/blob/master/errors/TypesDoNotUnify.md for more information,
or to contribute content related to this error.
Arafangion
  • 11,517
  • 1
  • 40
  • 72
  • As a clarification, I'm aware that `example :: (forall a. (Foo a) => a -> Int) -> Int` just magically works. But I don't understand why. If scoping was significant, then that implies that my first example in the question was really a `example :: forall b. (Foo b) => (a -> Int) -> Int`, which certainly shouldn't compile in purescript. – Arafangion May 05 '17 at 00:56
  • After discussing with coworkers, it appears that purescript effectively implements the haskell extension 'rank-n-types', and as such, https://ocharles.org.uk/blog/guest-posts/2014-12-18-rank-n-types.html is a fantastic explanation. Not sure how to best summarize this for stackoverflow, though. – Arafangion May 05 '17 at 04:21

1 Answers1

1

Compare

(1) example :: (forall a. (Foo a) => a -> Int) -> Int

with

(2) example :: forall a. (Foo a) => (a -> Int) -> Int

The latter essentially places responsibility on you, the caller, to supply as the argument to example a function (your choice!) w/ the signature a -> Int (such that there is a Foo instance for a).

The former, on the other hand, says that you, the caller, don't actually get to pick what this function a -> Int is. Rather, as Norman Ramsey has explained in a Haskell-related stackoverflow answer here, when the forall is "to the left" of the arrow (rather than "above the arrow") the implementation decides what function to supply. The signature in (2) is saying any function a -> Int will do as the argument to example (so long as there is a Foo intance for a).

If (1) just "magically" works, then, it's because the function that unwraps the newtype Bar is being selected by the compiler as perfectly satisfactory, and passed as the argument to example in case (1). After all, the signature of (1) suggests that example should return the same Int values no matter what function a -> Int is given (so long as there is a Foo instance for a). In case (2), the Int values returned by example may very well differ depending upon the specific function a -> Int supplied. The compiler cannot grab any such function that it knows satisfies the type at random. It cannot guess the type of a or a -> Int that you, the caller, actually have in mind.

Community
  • 1
  • 1
liminalisht
  • 1,243
  • 9
  • 11
  • What does my head in, is that in *both* cases, it is the caller that provides the function argument. In both cases 1, and 2, the caller has to provide, as the first argument, a function. Surely, my head rationalises, a Foo instance for `a` must exist in either case, so surely, they should be equivalent. – Arafangion May 06 '17 at 05:30
  • Yes but what are the constraints on this function that you can provide? In one case, you can provide any function from a to Int such that there is a Foo instance for a. In the other, the compiler knows a priori that you can only provide a function that doesnt actually use any knowledge about a except that it has a Foo instance. – liminalisht May 06 '17 at 06:31
  • What's the difference between those two cases? Given a pure function, which takes an `a`, and returns an `Int` making use of the `Foo` instance. It certainly can't inspect the value except via the type instance, can't it? (So, what use would any "knowledge" of the type give the compiler, except, ostensibly, for optimisation purposes...) – Arafangion May 06 '17 at 06:37
  • I've added another question here, which might be the same issue I am facing here, but I don't understand it. It might shed some light as to why I am finding it confusing: http://stackoverflow.com/questions/43817554/purescript-error-cant-match-equivalent-types – Arafangion May 06 '17 at 06:41
  • When you write (1) you promising there exists a fn that gets an Int from an a for all types a that have Foo instances. In case two, youre making no such promise that this fn exists for all a w Foo instances. What is confusing is that the forall when it is left of the arrow instead of above the arrow makes an existential promise. So the big difference bt (1) and (2) is that in (1) youre promising that such a fn exists for all as that have Foo instances, and in (2) you made no such promise. The compiler figured out in 1 that a must be Bar, bc only Bar has a Foo instance. – liminalisht May 06 '17 at 14:11