Ты же понимаешь, что первый для конкретного, а второй для всех?
давай вот такой пример newtype A a = A (a -> a) newtype B = B (forall a. a -> a) a :: A Int a = A (+ 1) b :: A Bool b = A not c :: B c = B id -- а больше вариантов и нет, нельзя придумать без всяких ансейфов и undefined-ов никаких больше функций с типом forall a. a->a кроме \x -> x
похожий пример есть в Thinking With Types, до этой степени я могу понять
ну тут то же самое по сути второй ContB это вроде бы то же самое что и Identity тип то есть мы можем сказать что между типом A и типом forall r. (A -> r) -> r есть изоморфизм to :: a -> ContB a to x = ContB \next -> next x from :: ContB a -> a from (ContB f) = f id то есть твой ContB a = Identity a = a по сути Identity A это "во мне значение A, распаковывай и используй, чтобы получить результат" ContB A это "я знаю A, скажи мне как ты его используешь и я отдам тебе результат".
Интересно, аforall r. a -> r значит, что функция должна выдавать значение для любого типа r? Но тогда может подойти только id, если я правильно понимаю
под эту сигнатуру id не подходит, только незавершающаяся функция подходит
А, ну да, точно, ведь id :: a -> a, а функция должна работать для любого r
Обсуждают сегодня