вопрос хаскельщикам

[juan_gandhi]

true x y = x
false x y = y

lampair :: a -> b -> (a -> b -> c) -> c
lampair x y p = p x y

pa :: ((a -> b -> c) ->c) -> a
pa p = p true

And I see

   • Couldn't match type ‘a’ with ‘c’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          pa :: forall a b c. ((a -> b -> c) -> c) -> a
        at sample1.hs:8:1-30
      ‘c’ is a rigid type variable bound by
        the type signature for:
          pa :: forall a b c. ((a -> b -> c) -> c) -> a
        at sample1.hs:8:1-30
      Expected type: a -> b -> c
        Actual type: c -> b -> c
    • In the first argument of ‘p’, namely ‘true’
      In the expression: p true
      In an equation for ‘pa’: pa p = p true
    • Relevant bindings include
        p :: (a -> b -> c) -> c (bound at sample1.hs:9:4)
        pa :: ((a -> b -> c) -> c) -> a (bound at sample1.hs:9:1)
  |

What have I done wrong? What fails here? Is Hindley-Milner "not smart enough"? What am I missing?

Comments

[sassa_nf]

No, I don't see that.

One of the problems is that there is a type a->b->c, but there is no function that can return a value of type c for any c.


a->b->c (type variables) is a family of functions.

a->b->a (type variables) is a family of functions included in the family of functions a->b->c.

You can pass any function from family a->b->a into a context expecting a->b->c, where at least c is not bound - which is to say, you can use any function from family a->b->a only where all functions a->b->c are allowed.

In pa :: ((a -> b -> c) ->c) -> a not all functions a->b->c are allowed.

[juan_gandhi]

Makes sense now. Proper quantifiers in proper places would clarify.

"Every ten minutes a man is mugged in the streets of New York. Now we are interviewing this man."

[sassa_nf]

More than that, "pa :: ((a -> b -> c) ->c) -> a" as declared is nonsense. It means pa is able to return a value of any given type a. You can't even construct such a (terminating) function.

So you can't return type a, you've got to return at most something of type c - as long as you can pass a function of type a->b->c for given a, b and c to a given function p. You can't even construct such a (terminating) function that can (construct and) pass such matching functions to p.

"p true" not matching the type is a minor problem compared to the two arguments above.