lomeo: (лямбда)
Dmitry Antonyuk ([personal profile] lomeo) wrote2007-04-10 02:31 pm

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

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

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


Запускал в GHCi 6.6

[identity profile] thesz.livejournal.com 2007-04-10 11:08 am (UTC)(link)
module A where

newtype Fun a = Fun (Fun a -> a)
 
fun x@(Fun f) = f x
 
myFix = fun (Fun fun)
Компилирую 'ghc -ddump-tc -c a.hs'. Тайпчекер выводит все правильно.

Может, это где-то еще?

[identity profile] lomeo.livejournal.com 2007-04-10 11:25 am (UTC)(link)
Наверное в моем компилере бага.
Кстати, если делаю -ddump-tc, то выводит типы верно, а потом опять подвисает.
Попробую переставить GHC, но позже.

Спасибо!

[identity profile] thesz.livejournal.com 2007-04-10 11:42 am (UTC)(link)
Забыл дополнить - у меня тоже 6.6.2 и тоже виснет.

Сейчас заменил newtype на data - все равно виснет.

Похоже, все же tc.

[identity profile] justbulat.livejournal.com 2007-04-12 03:03 pm (UTC)(link)
ещё 6.6.1 не вышел :D

[identity profile] thesz.livejournal.com 2007-04-12 04:27 pm (UTC)(link)
C:\...менты\Downloads\seen\SPARC\plans>ghc -v
Glasgow Haskell Compiler, Version 6.6.20061017, for Haskell 98, compiled by GHC
version 6.6.20061017
Using package config file: C:\ghc\ghc-6.6.20061224\package.conf
wired-in package base mapped to base-2.0
wired-in package rts mapped to rts-1.0
wired-in package haskell98 mapped to haskell98-1.0
wired-in package template-haskell mapped to template-haskell-2.0
Hsc static flags: -static
*** Deleting temp files:
Deleting:
*** Deleting temp dirs:
Deleting:
ghc.EXE: no input files
Usage: For basic information, try the `--help' option.
Вот. ;)

[identity profile] deni-ok.livejournal.com 2007-04-12 04:36 pm (UTC)(link)
Эээ... Может это год 2006?


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

[identity profile] thesz.livejournal.com 2007-04-12 04:52 pm (UTC)(link)
Видать.

У меня уже голова не варит.

[identity profile] migmit.livejournal.com 2007-04-10 11:26 am (UTC)(link)
Какая версия ghc? У меня, опять-таки, виснет.

[identity profile] thesz.livejournal.com 2007-04-10 11:43 am (UTC)(link)
6.6.2, тоже виснет, но типы выводит правильные (судя по -ddump-tc).

[identity profile] migmit.livejournal.com 2007-04-10 12:40 pm (UTC)(link)
Ну дык так бы сразу и сказал. У всех так.

[identity profile] thesz.livejournal.com 2007-04-10 12:54 pm (UTC)(link)
А непонятно, почему.

Я даже сигнатуры указал, все равно виснет.

[identity profile] palm-mute.livejournal.com 2007-04-10 03:09 pm (UTC)(link)
Аналогично, виснет.
Надо в кафе дядьке Саймону сообщить, однозначно баг.
А зачем такой myFix? Y-комбинатор не так определяется.

[identity profile] lomeo.livejournal.com 2007-04-10 03:23 pm (UTC)(link)
Знаю что не так. Баловался с нерекурсивным определением. Ты же сказал, что рекурсия, тем более хвостовая сосёт ;-)

В частности вот:

fixedFac f 0 = 1
fixedFac f n = n * f (n - 1)

fac = myFix fixedFac


Это хотел.

[identity profile] palm-mute.livejournal.com 2007-04-10 03:29 pm (UTC)(link)
Да я понял.
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

[identity profile] deni-ok.livejournal.com 2007-04-11 07:17 am (UTC)(link)
Здорово!
Какие вы оба умные :-)

[identity profile] lomeo.livejournal.com 2007-04-11 08:25 am (UTC)(link)
:-)

[identity profile] palm-mute.livejournal.com 2007-04-11 08:53 am (UTC)(link)
[Смайлик, ковыряющий в носу, уставившись в пол]

[identity profile] lomeo.livejournal.com 2007-04-10 03:28 pm (UTC)(link)
Y-комбинатор, кстати на Хаскеле не определяется, гранаты у него не той системы ;-)

[identity profile] palm-mute.livejournal.com 2007-04-10 03:31 pm (UTC)(link)
Почему? Я вроде комментом выше определил.
Все, убегаю с работы, до завтра.

[identity profile] lomeo.livejournal.com 2007-04-10 03:37 pm (UTC)(link)
Да, действительно, я прогнал, безтиповую лямбду то можно нарисовать, значит и Y можно.
До завтра!

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

[identity profile] nealar.livejournal.com 2007-04-11 06:42 am (UTC)(link)
Разве он будет её тип проверять?

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

[identity profile] lomeo.livejournal.com 2007-04-11 08:24 am (UTC)(link)
Не понял вопроса.

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

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

[identity profile] palm-mute.livejournal.com 2007-04-11 08:44 am (UTC)(link)
Я не согласен, что в моем примере выше есть бестиповая лямбда, там тип результата определяется переменной типа 'a'.
В конце концов, я ничего в твоем примере не изменил, кроме определения myfix.

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

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

[identity profile] lomeo.livejournal.com 2007-04-11 09:18 am (UTC)(link)
> Я не согласен, что в моем примере выше есть бестиповая лямбда, там тип результата определяется переменной типа 'a'.

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

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

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

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

[identity profile] palm-mute.livejournal.com 2007-04-11 09:31 am (UTC)(link)
> Это неважно, 'a' нужно лишь на нижнем уровне, когда мы применяем fix. selfApply и myfix - это же явно бестиповое использование (параметризуем Fun нужным значением, и получаем бестиповую лямбду).

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


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

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

[identity profile] lomeo.livejournal.com 2007-04-11 10:01 am (UTC)(link)
> Не уверен, что понимаю, что ты хочешь сказать.
Неважно. Я имел в виду, что Fun (Fun a -> a) эмулирует бестиповую лямбду, т.е. на нём можно сделать всё, что можно сделать на бестиповой лямбде. А 'a' тут есть или нет - роли не играет.

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

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

[identity profile] deni-ok.livejournal.com 2007-04-11 10:14 am (UTC)(link)
Что-то я не врубаюсь. Как ты, например, сделаешь
\x -> x x
?
myfix (\x -> x x) даст ошибку типизации. Или мы саму лямбду здесь должны делать по-другому?

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

[identity profile] lomeo.livejournal.com 2007-04-11 10:33 am (UTC)(link)
Если считать, что тип терма - Fun, а не Fun a ('a' нужен только для самого низа, когда мы к реальным вычислениям переходим), то всё ок - selfApply - это и есть твой \x -> x x ;-)

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

[identity profile] deni-ok.livejournal.com 2007-04-11 11:24 am (UTC)(link)
А, ну понял. Ты говоришь бестиповая лямбда, имея ввиду бестиповое исчисление. В смысле, что мы не ограниченны только типизируемыми выражениями.

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

[identity profile] lomeo.livejournal.com 2007-04-11 11:33 am (UTC)(link)
Наверное, я в терминах не очень

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

[identity profile] palm-mute.livejournal.com 2007-04-11 08:40 am (UTC)(link)
В бестиповом лямбда-исчислении все есть лямбда-терм - т.е. любой терм можно применить к любому терму и получить тоже терм. В просто-типизированном лямбда-исчислении такая загогулина непредставима, т.к. она имеет рекурсивный тип: 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: Замечание

[identity profile] palm-mute.livejournal.com 2007-04-11 08:50 am (UTC)(link)
Кстати, пока я игрался с этим примером, понял важное различие между newtype и data: если заменить data Untyped на newtype Untyped, printValue перестанет работать. Возможно, ни для кого это не новость, но меня удивило. Т.к. в случае newtype-декларации значения не имеют тега типа, следующее выражение возвращает "ok":
case (undefined :: Untyped) of (Untyped x) -> "ok"

Re: Замечание

[identity profile] lomeo.livejournal.com 2007-04-11 09:30 am (UTC)(link)
Интересное замечение, спасибо!

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

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

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

[identity profile] nealar.livejournal.com 2007-04-11 10:11 am (UTC)(link)
Вот почему у меня определения вида data Untyped = Untyped (Untyped -> Untyped)
никогда в голову не помещались! Моск уходил в бесконечную рекурсию.

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

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

[identity profile] lomeo.livejournal.com 2007-04-11 10:37 am (UTC)(link)
Рекурсия сама по себе сложна, а с типами так вообще. Т.к. функция (которую оборачивают Fun или Untyped) ковариантна по возвращаемому значению и контравариантна по параметрам, то говорят (я где то слышал), что Fun - контравариантнорекурсивный тип. Полагаю так у тебя в голове поместится :-]

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

[identity profile] nealar.livejournal.com 2007-04-11 10:49 am (UTC)(link)
Я и слов-то таких не знаю.
Ковариантный - это что-то из теормеха?

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

[identity profile] lomeo.livejournal.com 2007-04-11 11:35 am (UTC)(link)
хз, я в MIT'овском "Types And Programming Languages" читал, там в одном месте так назвали. А ещё где то читал с приставкой "рекурсивный".

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

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

[identity profile] palm-mute.livejournal.com 2007-04-11 12:20 pm (UTC)(link)
http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf

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

[identity profile] palm-mute.livejournal.com 2007-04-11 11:06 am (UTC)(link)
Не пойму, а где здесь ко- или контра- вариантность?

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

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

[identity profile] lomeo.livejournal.com 2007-04-11 11:52 am (UTC)(link)
По моему тоже, но за что купил, за то и продаю. Читал не в контексте Хаскеля, а просто что то из ТТ. Синоним для negative type recursion, т.е. когда рекурсивная переменная появляется слева от стрелки.

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

[identity profile] palm-mute.livejournal.com 2007-04-11 12:23 pm (UTC)(link)
>а просто что то из ТТ
А названием источника или даже ссылкой не поделишься?

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

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

[identity profile] lomeo.livejournal.com 2007-04-11 12:38 pm (UTC)(link)
Да, я тоже о таком определении знаю. Источником не поделюсь - не помню откуда :-( Можно поискать по negative type recursion contravariance, но у меня сейчас времени нет, к сожалению. Вечером погляжу.

Известная бага, оказывается

[identity profile] palm-mute.livejournal.com 2007-04-11 10:26 am (UTC)(link)
В Хаскелл-кафе мой вопрос еще не появился (во всяком случае, я его там не вижу), но Neil Mitchell уже ответил:

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: Известная бага, оказывается

[identity profile] lomeo.livejournal.com 2007-04-11 10:34 am (UTC)(link)
Спасибо!

[identity profile] thesz.livejournal.com 2007-04-12 04:28 pm (UTC)(link)
Начал читать комментарии.

Понял, что мозг навсегда испорчен Майкрософт Прожект.

Ушел горевать.