newtype Fun a = Fun (Fun a -> a)
unwrap (Fun f) = f
selfApply f = unwrap f f
myfix f = selfApply $ Fun $ \g -> f (selfApply g)
> myfix (\f n -> if n==0 then 1 else n * f (n-1)) 5
120
Я имею в виду, что напрямую объявить Y комбинатор в Haskell нельзя - там тип получается бесконечный. Но если мы сделаем безтиповую лямбду (как в примере palm_mute), то можно.
Я не согласен, что в моем примере выше есть бестиповая лямбда, там тип результата определяется переменной типа 'a'. В конце концов, я ничего в твоем примере не изменил, кроме определения myfix.
Кстати, ты не надумал запостить куда-нибудь баг-репорт? Как бы там ни было, а компилятор виснуть не должен.
> Я не согласен, что в моем примере выше есть бестиповая лямбда, там тип результата определяется переменной типа 'a'.
Это неважно, 'a' нужно лишь на нижнем уровне, когда мы применяем fix. selfApply и myfix - это же явно бестиповое использование (параметризуем Fun нужным значением, и получаем бестиповую лямбду).
> Кстати, ты не надумал запостить куда-нибудь баг-репорт? Как бы там ни было, а компилятор виснуть не должен.
Я пробовал как то писать на haskell мейл листы, у меня не проходило почему то письмо. Уходило - да, а затем как в омут. хз.
> Это неважно, 'a' нужно лишь на нижнем уровне, когда мы применяем fix. selfApply и myfix - это же явно бестиповое использование (параметризуем Fun нужным значением, и получаем бестиповую лямбду).
Не уверен, что понимаю, что ты хочешь сказать. Бестиповая лямбда имеет тип (Untyped -> Untyped) as Untyped, из нее невозможно получить список или число, а из Fun a - можно. Тип бестипового лямбда-выражения можно выразить с помощью рекурсивных типов, но это не означает, что любое применение рекурсивных типов равносильно отсутствию типов. Тайп-чекер замечательно контролирует типы при работе со списками, типы f и n в теле функции факториала тоже определены.
>Я пробовал как то писать на haskell мейл листы, у меня не проходило почему то письмо. Уходило - да, а затем как в омут. хз. У меня получалось, я могу попробовать.
> Не уверен, что понимаю, что ты хочешь сказать. Неважно. Я имел в виду, что Fun (Fun a -> a) эмулирует бестиповую лямбду, т.е. на нём можно сделать всё, что можно сделать на бестиповой лямбде. А 'a' тут есть или нет - роли не играет.
Что-то я не врубаюсь. Как ты, например, сделаешь \x -> x x ? myfix (\x -> x x) даст ошибку типизации. Или мы саму лямбду здесь должны делать по-другому?
Если считать, что тип терма - Fun, а не Fun a ('a' нужен только для самого низа, когда мы к реальным вычислениям переходим), то всё ок - selfApply - это и есть твой \x -> x x ;-)
В бестиповом лямбда-исчислении все есть лямбда-терм - т.е. любой терм можно применить к любому терму и получить тоже терм. В просто-типизированном лямбда-исчислении такая загогулина непредставима, т.к. она имеет рекурсивный тип: LambdaTerm = (LambdaTerm->LambdaTerm). Но в любом языке с рекурсивными типами тип бестипового лямбда терма можно легко закодировать:
module UntypedLambda where
import Prelude hiding(and, or)
data Untyped = Untyped (Untyped -> Untyped)
apply (Untyped f) x = f x
true = Untyped $ \x -> Untyped $ \y -> x
false = Untyped $ \x -> Untyped $ \y -> y
or x y = (x `apply` true) `apply` y
and x y = (x `apply` y) `apply` false
uif cond then_ else_ = (cond `apply` then_) `apply` else_
-- tests
t1 = true `or` (true `and` false)
t2 = false `and` true
t3 = (false `and` false) `or` (true `and` true)
t4 = Untyped $ \_ -> true
-- этот фокус нам нужен, чтобы выковырять значение из
-- бестипового лямбда-терма
printValue u =
case (uif u (error "true") (error "false")) of
(Untyped _) -> error "Not boolean value"
Ok, modules loaded: UntypedLambda.
*UntypedLambda> printValue t1
*** Exception: true
*UntypedLambda> printValue t2
*** Exception: false
*UntypedLambda> printValue t3
*** Exception: true
*UntypedLambda> printValue t4
*** Exception: Not boolean value
*UntypedLambda>
Кстати, пока я игрался с этим примером, понял важное различие между newtype и data: если заменить data Untyped на newtype Untyped, printValue перестанет работать. Возможно, ни для кого это не новость, но меня удивило. Т.к. в случае newtype-декларации значения не имеют тега типа, следующее выражение возвращает "ok":
case (undefined :: Untyped) of (Untyped x) -> "ok"
Рекурсия сама по себе сложна, а с типами так вообще. Т.к. функция (которую оборачивают Fun или Untyped) ковариантна по возвращаемому значению и контравариантна по параметрам, то говорят (я где то слышал), что Fun - контравариантнорекурсивный тип. Полагаю так у тебя в голове поместится :-]
По моему тоже, но за что купил, за то и продаю. Читал не в контексте Хаскеля, а просто что то из ТТ. Синоним для negative type recursion, т.е. когда рекурсивная переменная появляется слева от стрелки.
>а просто что то из ТТ А названием источника или даже ссылкой не поделишься?
Я описание ко- и контра- вариантности видел в TAPL и в статьях Карделли, там все просто и прозрачно - вводится отношение subtyping (как по-русски? "подтипизация"?) между функциями при наличии subtyping между типами аргумента и результата: a -> b <: a' -> b', если a' <: a и b <: b'
Да, я тоже о таком определении знаю. Источником не поделюсь - не помню откуда :-( Можно поискать по negative type recursion contravariance, но у меня сейчас времени нет, к сожалению. Вечером погляжу.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
no subject
Может, это где-то еще?
no subject
Кстати, если делаю -ddump-tc, то выводит типы верно, а потом опять подвисает.
Попробую переставить GHC, но позже.
Спасибо!
no subject
Сейчас заменил newtype на data - все равно виснет.
Похоже, все же tc.
no subject
no subject
no subject
We are aiming for a 6.6.1 release candidate on the 6th April, and release on the 20th April.
отсюда http://hackage.haskell.org/trac/ghc
no subject
У меня уже голова не варит.
no subject
no subject
no subject
no subject
Я даже сигнатуры указал, все равно виснет.
no subject
Надо в кафе дядьке Саймону сообщить, однозначно баг.
А зачем такой myFix? Y-комбинатор не так определяется.
no subject
В частности вот:
Это хотел.
no subject
no subject
Какие вы оба умные :-)
no subject
no subject
no subject
no subject
Все, убегаю с работы, до завтра.
no subject
До завтра!
Не понял, почему
Re: Не понял, почему
Я имею в виду, что напрямую объявить Y комбинатор в Haskell нельзя - там тип получается бесконечный. Но если мы сделаем безтиповую лямбду (как в примере
Re: Не понял, почему
В конце концов, я ничего в твоем примере не изменил, кроме определения myfix.
Кстати, ты не надумал запостить куда-нибудь баг-репорт? Как бы там ни было, а компилятор виснуть не должен.
Re: Не понял, почему
Это неважно, 'a' нужно лишь на нижнем уровне, когда мы применяем fix. selfApply и myfix - это же явно бестиповое использование (параметризуем Fun нужным значением, и получаем бестиповую лямбду).
> Кстати, ты не надумал запостить куда-нибудь баг-репорт? Как бы там ни было, а компилятор виснуть не должен.
Я пробовал как то писать на haskell мейл листы, у меня не проходило почему то письмо. Уходило - да, а затем как в омут. хз.
Re: Не понял, почему
Не уверен, что понимаю, что ты хочешь сказать. Бестиповая лямбда имеет тип (Untyped -> Untyped) as Untyped, из нее невозможно получить список или число, а из Fun a - можно.
Тип бестипового лямбда-выражения можно выразить с помощью рекурсивных типов, но это не означает, что любое применение рекурсивных типов равносильно отсутствию типов. Тайп-чекер замечательно контролирует типы при работе со списками, типы f и n в теле функции факториала тоже определены.
>Я пробовал как то писать на haskell мейл листы, у меня не проходило почему то письмо. Уходило - да, а затем как в омут. хз.
У меня получалось, я могу попробовать.
Re: Не понял, почему
Неважно. Я имел в виду, что Fun (Fun a -> a) эмулирует бестиповую лямбду, т.е. на нём можно сделать всё, что можно сделать на бестиповой лямбде. А 'a' тут есть или нет - роли не играет.
> У меня получалось, я могу попробовать.
Давай!
Re: Не понял, почему
\x -> x x
?
myfix (\x -> x x) даст ошибку типизации. Или мы саму лямбду здесь должны делать по-другому?
Re: Не понял, почему
Re: Не понял, почему
Re: Не понял, почему
Re: Не понял, почему
module UntypedLambda where import Prelude hiding(and, or) data Untyped = Untyped (Untyped -> Untyped) apply (Untyped f) x = f x true = Untyped $ \x -> Untyped $ \y -> x false = Untyped $ \x -> Untyped $ \y -> y or x y = (x `apply` true) `apply` y and x y = (x `apply` y) `apply` false uif cond then_ else_ = (cond `apply` then_) `apply` else_ -- tests t1 = true `or` (true `and` false) t2 = false `and` true t3 = (false `and` false) `or` (true `and` true) t4 = Untyped $ \_ -> true -- этот фокус нам нужен, чтобы выковырять значение из -- бестипового лямбда-терма printValue u = case (uif u (error "true") (error "false")) of (Untyped _) -> error "Not boolean value" Ok, modules loaded: UntypedLambda. *UntypedLambda> printValue t1 *** Exception: true *UntypedLambda> printValue t2 *** Exception: false *UntypedLambda> printValue t3 *** Exception: true *UntypedLambda> printValue t4 *** Exception: Not boolean value *UntypedLambda>Re: Замечание
Re: Замечание
Там действительно вместо (Untyped x) будет матчиться x wrapped типа, значит undefined просто не будет выполнен.
Надо запомнить - pattern matching для newtype ленив, если он в виде (C a) ;-)
Re: Не понял, почему
никогда в голову не помещались! Моск уходил в бесконечную рекурсию.
Получается, типы навроде Fun a = Fun (Fun a -> a) как раз для того всегда и делаются, чтоб обмануть тайпчекер?
Re: Не понял, почему
Re: Не понял, почему
Ковариантный - это что-то из теормеха?
Re: Не понял, почему
Честно, это не я придумал :-)
Re: Не понял, почему
Мощно завернул!
По моему разумению, о ко(контра)вариантности можно говорить только при наличии subtyping между типами аргументов или результата.
Всего лишь повторил мощно завернутое ;-)
Re: Всего лишь повторил мощно завернутое ;-)
А названием источника или даже ссылкой не поделишься?
Я описание ко- и контра- вариантности видел в TAPL и в статьях Карделли, там все просто и прозрачно - вводится отношение subtyping (как по-русски? "подтипизация"?) между функциями при наличии subtyping между типами аргумента и результата:
a -> b <: a' -> b', если a' <: a и b <: b'
Re: Всего лишь повторил мощно завернутое ;-)
Известная бага, оказывается
It's a documented bug in GHC:
http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html#bugs-ghc
"GHC's inliner can be persuaded into non-termination using the
standard way to encode recursion via a data type"
Thanks
Neil
Re: Известная бага, оказывается
no subject
Понял, что мозг навсегда испорчен Майкрософт Прожект.
Ушел горевать.