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

[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

[lomeo]

Так первый аргумент pa, который p, принимает функцию (a -> b -> c), а мы ей передаём true, который a -> b -> a.

Например, предположим мы имеем
foo :: (Int -> String -> Bool) -> Bool
и вызываем p foo, очевидно, что foo не может принимать true.

Если c поменять на a, то всё сойдётся, не знаю, нужно ли это. Что предполагается получить?

[juan_gandhi]

Я знаю, что если c поменять на a, то сойдется. Но я наивно полагал, что функция типа a->b->a - это частный случай функции типа a->b->c.

Вот, например, скала:

scala> type F2[A,B,C] = A => B => C
defined type alias F2

scala> type P1[A,B] = F2[A,B,A]
defined type alias P1

scala> def p1[A,B]: P1[A,B] = (a:A) => (b:B) => a
p1: [A, B]=> A => (B => A)

Уж не в том ли проблема, что типы Черча в некотором смысле не столь, э, сильны, как типы Карри?

[lomeo]

У нас тут функция в функции, следовательно этот a->b->c в ковариантной позиции, а значит, a->b->a нельзя применить вместо a->b->c.

Например, если мы переведём её опять в контравариантную позицию, то можно:

> { pb :: (((a -> b -> c) -> c) -> a) -> a; pb p = p (\f -> f undefined undefined) }
> :t pb (\f -> f true)
pb (\f -> f true) :: c

[juan_gandhi]

Хм, любопытно.

[lomeo]

Да! И в скале этот код тоже не скомпилируется:

def tru[A,B](a: A, b: B): A = a
def pa[A, B, C](p: ((A, B) => C) => C): A = p(tru)

Контравариантная у нас super, а ковариантная extends. В терминах Java. В терминах Scala - и +.

Обратный пример тоже на всякий случай покажу. Вот это компилируется:

def foo[A,B,C](a: A, b: B): C = ???
def pa[A, B, C](p: ((A,B) => A) => A): A = p(foo)

Типы поменялись местами по сравнению с первым примером (у нас принимает более общий тип в том месте, где мы ожидаем более конкретный. Хотя я предпочитаю так не рассуждать, а просто пробежаться по стрелочками и посчитать в какой позиции аргумент.

[juan_gandhi]

Да без разницы, по стрелочкам или просто сообразить вариантность. Не должно "почему-то" работать. Надо нарисовать категорно будет (это я и в уме могу).

Вот что читаю: https://ifl2014.github.io/submissions/ifl2014_submission_13.pdf - и поразило, что swap нельзя так просто написать.

Но вот так работает:

scala> type F2[A,B,C] = A => B => C
defined type alias F2

scala> type P1[A,B] = F2[A,B,A]
defined type alias P1

scala> def p1[A,B]: P1[A,B] = (a:A) => (b:B) => a
p1: [A, B]=> A => (B => A)

[lomeo]

Я статью не читал, но в Чёрче вроде как swap (если речь о swap пары) делается просто:

> tuple = \x y z -> z x y
> first = \t -> t (\x y -> x)
> second = \t -> t (\x y -> y)
> swap = \t f -> t (\x y -> f y x)
> x = tuple 1 2
> first x
1
> second x
2
> y = swap x
> first y
2
> second y
1

Статью потом прочту, уже час ночи, спать пора.

[juan_gandhi]

А, хитро. В смысле, я это и хотел нарисовать, но тут хитро, лямбды просто вставляем. А если эти лямбды вынуть?

[sassa_nf]

Prelude> first = \t -> t (\x y -> x)
Prelude> :t first
first :: ((t1 -> t2 -> t1) -> t) -> t

That is, if you don't use lambdas, you get your code, but with the corrected types :)

pa :: ((a->b->a)->c)->c

[sassa_nf]

Yes, but even if it is, is (a->b->a)->c a subtype of (a->b->c)->c?

[sassa_nf]

Hang on a minute.

A->B->A (specific types) is a special case of a->b->c (type variables) in some sense.

Where did you get a->b->a (type variables) being a special case of a->b->c?

[juan_gandhi]

That's a special case when c = a, no?

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

[sassa_nf]

It's pretty clear that you don't return type different from the type returned by p. So the type signature of pa should end with ...->d)->d.

Then specifying that argument is of type (a->b->c)->c means the argument is allowed to be bound to _any_ three types, so true does not fit, because it forces the return type to be the same as the first argument.

Prelude> true x y = x
Prelude> :t true
true :: t -> t1 -> t
Prelude> pa p = p true
Prelude> :t pa
pa :: ((t1 -> t2 -> t1) -> t) -> t

You probably can get away with nesting the predicate - to express that the function p should be polymorphic of a and b.

...and you can! (ghci -XRankNTypes)

Prelude> pa :: (forall a b. (a->b->c)->d)->d; pa p = p true

[sassa_nf]

All these polymorphic shenanigans become less of a magic, when you start passing the type around explicitly, like in Agda.

(Also, could think of how polymorphism / typeclasses work: you've got to pass the pointer to instance / implementation table)

pa : (A B C : Set) -> ((A -> B -> C) -> C) -> A

(this is equivalent to your first declaration)

is obviously different from

pa : (A C : Set) -> ((B : Set) -> (A -> B -> C) -> C) -> A

(is not meant to work as a type for pa p = p true, just an example)

different from

pa : (C D : Set) -> ((A B : Set) -> (A -> B -> C) -> D) -> D

(the actual thing that works)

and different from

pa : (C : Set) -> (((A B : Set) -> A -> B -> C) -> C) -> C

You see, when you declare the types are on input, it means that the call site literally can "choose" any values for types, and it will work.

So in your example (the first declaration here) the caller can choose any A, B and C, and yet you pass a specific instance true, which is not polymorphic in return type - it binds C to be the same as A. You did not express this to be the case, so the caller of pa cannot tell that A and C must be bound in some specific way. (This reference to a "caller" is a rather mechanical way of explaining; something like the intuition behind it. I am sure type theory has the actual explanation.)

Similarly in the third case you tell the caller that pa decides what the types A and B are, so the caller of pa must pass a p that can accept any A and B.

The fourth case is different yet again - you tell the caller that p can decide what the types A and B are, whereas C is still determined by the caller directly, so pa will make sure it will pass such a function that works. (true does not match the description, because it is (A B : Set) -> A -> B -> A, not (A B C : Set) -> A -> B -> C - it does not produce a value of any given type C)

---

Also, once you write the types down like this, it is obvious that even though the types join up in the third case, there is no way a function p can be instantiated, except a const, perhaps - there is no way p can construct a value for any A and B it is given by pa.

[anonim_legion]

А вы в телеграме спросите, в чате @haskellru. Там постоянно кто-то есть.

[juan_gandhi]

О, вот и полезная область телеграма. Спасибо!

[pbl]

I just wanted to say that:

- I'm surprised this surprises you.
- What sassa_nf is saying above is very much to the point.
- I honestly think you're going backwards about this when you're talking about doing this "категорно". Just start out with proper Λ/Π and no :>, everything is gonna make sense. Once it does, I guess you could always do this "категорно", although I wouldn't know anything about that, obviously...

[juan_gandhi]

I'm surprised too.
Regarding expressing stuff categorically, it's a very interesting question I'm thinking about now. But rather in the opposite direction, categories in lambda.