Простые задачки на Карри-Говарда

[deni_ok]

Доказать, используя Хаскель, что следующие тавтологии верны интуиционистски
(a -> c) /\ (b -> c) -> a \/ b -> c (a \/ b -> c) -> (a -> c) /\ (b -> c) (Понятно, что конъюнкция - это пара, а дизъюнкция - Either.)

UPD. Стоит напомнить, что изоморфизм Карри-Говарда имеет место между интуиционистской версией пропозициональной логики и подмножеством

Comments

[ex_juan_gan]

Прелесть какая. А как это в Хаскеле "верность интуиционистски" вообще доказывается? Уж не написанием ли кода?

[deni_ok]

Да, именно так. Но, конечно, на подмножестве Хаскеля без рекурсии , иначе система not sound: fix :: (a -> a) -> a.

[migmit]

И без рекурсивных типов в том числе.

[deni_ok]

Да, data Mu f = In (f (Mu f)) и тому подобное тоже, конечно, все попортит.

[rvp74]

для первого как-то сразу код в голову пришел:

ex1 :: (a -> c, b -> c) -> Either a b -> c
ex1 (f,g) = h where
h (Left l) = f l
h (Right r) = g r

[rvp74]

второй почему-то сразу не дался, но решение оказалось еще проще:

ex2 :: (Either a b -> c) -> (a -> c, b -> c)
ex2 h = (h . Left, h . Right)

[voidex]

1.
uncurry (|||)
2.
(. Left) &&& (. Right)

[deni_ok]

Стрелочник.

[sassa_nf]

import Control.Arrow
f :: (a->c, b->c) -> Either a b -> c
f = uncurry (|||)

g :: (Either a b -> c) -> (a->c, b->c)
g = (.Left) &&& (.Right)

[deni_ok]

Еще один стрелочник.