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

[lomeo]

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

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

Запускал в GHCi 6.6

Comments

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

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