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

[lomeo]

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

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

Запускал в GHCi 6.6

Comments

[lomeo.livejournal.com]

Да, действительно, я прогнал, безтиповую лямбду то можно нарисовать, значит и Y можно.
До завтра!

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

[nealar.livejournal.com]

Разве он будет её тип проверять?

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]

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

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

[palm-mute.livejournal.com]

В бестиповом лямбда-исчислении все есть лямбда-терм - т.е. любой терм можно применить к любому терму и получить тоже терм. В просто-типизированном лямбда-исчислении такая загогулина непредставима, т.к. она имеет рекурсивный тип: 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> 

Re: Замечание

[palm-mute.livejournal.com]

Кстати, пока я игрался с этим примером, понял важное различие между newtype и data: если заменить data Untyped на newtype Untyped, printValue перестанет работать. Возможно, ни для кого это не новость, но меня удивило. Т.к. в случае newtype-декларации значения не имеют тега типа, следующее выражение возвращает "ok":

case (undefined :: Untyped) of (Untyped x) -> "ok"

Re: Замечание

[lomeo.livejournal.com]

Интересное замечение, спасибо!

Там действительно вместо (Untyped x) будет матчиться x wrapped типа, значит undefined просто не будет выполнен.

Надо запомнить - pattern matching для newtype ленив, если он в виде (C a) ;-)

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

[nealar.livejournal.com]

Вот почему у меня определения вида data Untyped = Untyped (Untyped -> Untyped)
никогда в голову не помещались! Моск уходил в бесконечную рекурсию.

Получается, типы навроде Fun a = Fun (Fun a -> a) как раз для того всегда и делаются, чтоб обмануть тайпчекер?

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

[lomeo.livejournal.com]

Рекурсия сама по себе сложна, а с типами так вообще. Т.к. функция (которую оборачивают Fun или Untyped) ковариантна по возвращаемому значению и контравариантна по параметрам, то говорят (я где то слышал), что Fun - контравариантнорекурсивный тип. Полагаю так у тебя в голове поместится :-]

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

[nealar.livejournal.com]

Я и слов-то таких не знаю.
Ковариантный - это что-то из теормеха?

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

[lomeo.livejournal.com]

хз, я в MIT'овском "Types And Programming Languages" читал, там в одном месте так назвали. А ещё где то читал с приставкой "рекурсивный".

Честно, это не я придумал :-)

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

[palm-mute.livejournal.com]

http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf

Мощно завернул!

[palm-mute.livejournal.com]

Не пойму, а где здесь ко- или контра- вариантность?

По моему разумению, о ко(контра)вариантности можно говорить только при наличии subtyping между типами аргументов или результата.

Всего лишь повторил мощно завернутое ;-)

[lomeo.livejournal.com]

По моему тоже, но за что купил, за то и продаю. Читал не в контексте Хаскеля, а просто что то из ТТ. Синоним для negative type recursion, т.е. когда рекурсивная переменная появляется слева от стрелки.

Re: Всего лишь повторил мощно завернутое ;-)

[palm-mute.livejournal.com]

>а просто что то из ТТ
А названием источника или даже ссылкой не поделишься?

Я описание ко- и контра- вариантности видел в TAPL и в статьях Карделли, там все просто и прозрачно - вводится отношение subtyping (как по-русски? "подтипизация"?) между функциями при наличии subtyping между типами аргумента и результата:
a -> b <: a' -> b', если a' <: a и b <: b'

Re: Всего лишь повторил мощно завернутое ;-)

[lomeo.livejournal.com]

Да, я тоже о таком определении знаю. Источником не поделюсь - не помню откуда :-( Можно поискать по negative type recursion contravariance, но у меня сейчас времени нет, к сожалению. Вечером погляжу.