Why don't these types unify when using type co

2019-09-14 17:14发布

问题:

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.

回答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.



标签: purescript