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

[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]

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.