Что меня удивляет:

топ 100 блогов ru_declarative — 23.02.2010 Если имеется: &forall b (∀ a (P (a) &rArr Q (b)) ⇒ Q (b))

Поскольку &forall a P (a) &rArr Q (b) ≡ ∃ a (P (a) ⇒ Q (b)), то

∀ b ∃ a ( (P (a) &rArr Q (b)) &rArr Q (b)), и поскольку (A ⇒ B) ⇒ B ≡ A, то

∃ a P (a)


Так вот - что меня удивляет, что экзистенциальные типы в Haskell действительно так выражаются, через универсальный полиморфизм:
type Ex = forall b . (forall a . Show a ⇒ a → b) → b
pack :: Show v ⇒ v → Ex
pack v = λ fn → fn v
one = pack 1
str = pack "Str"
main = do one print; str print

И это и правда работает:
msk@kouzdra-nest:~/TEST$ ghc -fglasgow-exts exist.hs -o exist && ./exists 
1
"Str"

Оставить комментарий

Предыдущие записи блогера :
Архив записей в блогах:
Живёт себе человек, 50-ти лет, через пять лет собиралась на пенсию, всё рассчитала чотенько, планы запланировала, работает "покамест" (дурацкое слово, хрень и мусор языка, зачем я его вообще вспомнила?) А ту вдруг грят с небес - неа, будешь ещё восьмерёху тянуть сверх. Это вообще как? ...
И кто придумал эти учебы и занимания, как говорит сын Витя?:)С каждым днем жизнь ...
Доброго всем вечера. Очевидно что Эльга - жена Владимира Соловьёва - сильно постарела. Время не щадит людей - мы все стареем - кроме самого Володии; он, как вы сами видите - как был пятилетним пацаном, так им и остаётся. Молоть всякую чушь напропалую - не это ли элексир молодости ? А ...
Matt Drudge пишет : I've linked to @washingtonpost over 10,000X in 25 years of doing DRUDGEREPORT. I currently give them 37% of their referral traffic, according to http://similarweb.com . It's a brutal business. Not even a thank you. Instead: YOU'RE A RUSSIAN OPERATIVE! Тут вот что ...
С воскресных посиделок Так держать! / What a Way to Go! / 1964 Луиза Мей Фостер романтичная молодая женщина, которая мечтает выйти замуж по любви, а не за деньги. Однако на ней словно лежит проклятье, потому что все ее мужья - так или иначе - не могут устоять перед соблазном ...