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

[lomeo]

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

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

Запускал в GHCi 6.6

Comments

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