Вывод типов всегда завершается, говорите?

[lomeo]

Вот здесь у меня висит на выводе типа myFix:

newtype Fun a = Fun (Fun a -> a)
 
fun x@(Fun f) = f x
 
myFix = fun (Fun fun)

Запускал в GHCi 6.6

Comments

Re: Не понял, почему

[lomeo.livejournal.com]

Не понял вопроса.

Я имею в виду, что напрямую объявить Y комбинатор в Haskell нельзя - там тип получается бесконечный. Но если мы сделаем безтиповую лямбду (как в примере palm_mute), то можно.

Re: Не понял, почему

[palm-mute.livejournal.com]

Я не согласен, что в моем примере выше есть бестиповая лямбда, там тип результата определяется переменной типа 'a'.
В конце концов, я ничего в твоем примере не изменил, кроме определения myfix.

Кстати, ты не надумал запостить куда-нибудь баг-репорт? Как бы там ни было, а компилятор виснуть не должен.

Re: Не понял, почему

[lomeo.livejournal.com]

> Я не согласен, что в моем примере выше есть бестиповая лямбда, там тип результата определяется переменной типа 'a'.

Это неважно, 'a' нужно лишь на нижнем уровне, когда мы применяем fix. selfApply и myfix - это же явно бестиповое использование (параметризуем Fun нужным значением, и получаем бестиповую лямбду).

> Кстати, ты не надумал запостить куда-нибудь баг-репорт? Как бы там ни было, а компилятор виснуть не должен.

Я пробовал как то писать на haskell мейл листы, у меня не проходило почему то письмо. Уходило - да, а затем как в омут. хз.

Re: Не понял, почему

[palm-mute.livejournal.com]

> Это неважно, 'a' нужно лишь на нижнем уровне, когда мы применяем fix. selfApply и myfix - это же явно бестиповое использование (параметризуем Fun нужным значением, и получаем бестиповую лямбду).

Не уверен, что понимаю, что ты хочешь сказать. Бестиповая лямбда имеет тип (Untyped -> Untyped) as Untyped, из нее невозможно получить список или число, а из Fun a - можно.
Тип бестипового лямбда-выражения можно выразить с помощью рекурсивных типов, но это не означает, что любое применение рекурсивных типов равносильно отсутствию типов. Тайп-чекер замечательно контролирует типы при работе со списками, типы f и n в теле функции факториала тоже определены.


>Я пробовал как то писать на haskell мейл листы, у меня не проходило почему то письмо. Уходило - да, а затем как в омут. хз.
У меня получалось, я могу попробовать.

Re: Не понял, почему

[lomeo.livejournal.com]

> Не уверен, что понимаю, что ты хочешь сказать.
Неважно. Я имел в виду, что Fun (Fun a -> a) эмулирует бестиповую лямбду, т.е. на нём можно сделать всё, что можно сделать на бестиповой лямбде. А 'a' тут есть или нет - роли не играет.

> У меня получалось, я могу попробовать.
Давай!

Re: Не понял, почему

[deni-ok.livejournal.com]

Что-то я не врубаюсь. Как ты, например, сделаешь
\x -> x x
?
myfix (\x -> x x) даст ошибку типизации. Или мы саму лямбду здесь должны делать по-другому?

Re: Не понял, почему

[lomeo.livejournal.com]

Если считать, что тип терма - Fun, а не Fun a ('a' нужен только для самого низа, когда мы к реальным вычислениям переходим), то всё ок - selfApply - это и есть твой \x -> x x ;-)

Re: Не понял, почему

[deni-ok.livejournal.com]

А, ну понял. Ты говоришь бестиповая лямбда, имея ввиду бестиповое исчисление. В смысле, что мы не ограниченны только типизируемыми выражениями.

Re: Не понял, почему

[lomeo.livejournal.com]

Наверное, я в терминах не очень