Вопрос по генерации кода для GADTs.

[Alexander V Vershilov]

Здравствуйте.

У меня возникла небольшая проблема с пониманием правил для
GADTs в итоге поведение генерируемого ghc кода отличатся от ожидаемого,
не могли бы вы помочь мне и объяснить почему это происходит, или где
искать ошибку. Ниже lhs-код комментариями, код является минимальным
примером некорректного поведения (в реальном проекте все чуть-чуть сложнее
и все введенные функции не случайны)

> {-# LANGUAGE ExistentialQuantification #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE GADTs #-}
> module Main where

> import Foreign
> import Unsafe.Coerce

тип описывающий возможные типы значений

> data M = A | B deriving (Show, Eq)

в реальном проекте это указатель на сишную кучу

> newtype S (a :: M) = S Int

специальный тип введенный для того, чтобы была
возможность возвращать значения типа не известного
на этапе компиляции

> data SomeS = forall a . SomeS (S a)

View-тип для отображения структуры данных на которые
указывает указатель из S, две штуки для наглядности
результатов


> data V0 :: M -> * where
> V0A :: Int -> V0 A
> V0B :: Double -> V0 B

> data V1 :: M -> * where
> V1A :: Int -> V1 A
> V1B :: Double -> V1 B
> V1a :: () -> V1 a


Создание View-типа (в реальном проекте сделано через
получение данных из Storable), тут мне не нравится,
но во всех частях проекта (кроме того о котором вопрос)
код работает верно.

> viewV0 :: S a -> V0 a
> viewV0 (S i) | even i = unsafeCoerce $ V0A 1
> | otherwise = unsafeCoerce $ V0B 2


> viewV1:: S a -> V1 a
> viewV1 (S i) | even i = unsafeCoerce $ V1A 1
> | otherwise = unsafeCoerce $ V1B 2


Получение реального типа выражения S

> typeOf :: S a -> M
> typeOf (S i) = if (even i) then A else B

Преобразование типа от обобщенного к конкретному. В этом
месте содержится ошибка, т.к. тип S a зависит только от того,
как он может использоваться и не зависит от M. (Если переписать
код с использованием singletons и связать SM a и результат S a
то проблема исчезет, но в данном случае интересно именно поведение
при полиморфном результате)

> cast :: M -> SomeS -> S a
> cast ty (SomeS s@(S i))
> | ty == typeOf s = S i
> | otherwise = error "cast"

Проверка, тут интересны 3 теста:

> test0 :: IO ()
> test0 =
> let s = cast A (SomeS (S 0))
> in case viewV0 s of
> V0A{} -> putStrLn "test0 - A"
> V0B{} -> putStrLn "test0 - B"

> test1 :: IO ()
> test1 =
> let s = cast A (SomeS (S 2)) :: S A
> in case viewV0 s of
> V0A{} -> putStrLn "test1 - A"

> test2 :: IO ()
> test2 =
> let s = cast A (SomeS (S 4))
> in case viewV1 s of
> V1A{} -> putStrLn "test2 - A"
> V1B{} -> putStrLn "test2 - B"
> V1a{} -> putStrLn "test2 - O_o"

Результат выполнения этого кода достаточно неожиданен,
* первый тест не выведет ничего
* второй тест вывод как и ожидается A
* третий тест выводит "O_o"

Получается, что при case по GADT имеющему полиморфный тип
(V GHC.Prim.Any) происходит матчинг только по тем конструкторам,
которые имеют тип V a? так и задумано или тут проблема?

--
Alexander

[Antonio Nikishaev]

Ну тип-то у него получается ‘V1 a’. Как иначе?

> --
> Вы получили это сообщение, поскольку подписаны на группу Русский Haskell.
>
> Чтобы отменить подписку на эту группу и больше не получать от нее сообщения, отправьте письмо на электронный адрес haskell-russi...@googlegroups.com.
> Чтобы добавлять сообщения в эту группу, отправьте письмо по адресу haskell...@googlegroups.com.
> Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/CAO-1Pb55UZHMu6uTcit_j56qktO9VxmcbZm2LftmUqULX1W0Dg%40mail.gmail.com.
> Настройки подписки и доставки писем: https://groups.google.com/d/optout.

[Alexander V Vershilov]

Не могли бы вы немного распространить ответ?

Просто иначе - в случае если тип выводится, как  V1 GHC.Prim.Any делать честный матчинг по всем конструкторам указанным в case, даже в том случае, если там есть полиморфные типы то выбирать тот, у которого конструктор подходит, а не первый подходящий при объявлении.

Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/71D0FEF7-59DB-457C-9221-F6BEC4135461%40gmail.com.

[Antonio Nikishaev]

On 30 Jul 2014, at 18:08, Alexander V Vershilov <alexander...@gmail.com> wrote:

> Не могли бы вы немного распространить ответ?

> Просто иначе - в случае если тип выводится, как V1 GHC.Prim.Any делать честный матчинг по всем конструкторам указанным в case, даже в том случае, если там есть полиморфные типы то выбирать тот, у которого конструктор подходит, а не первый подходящий при объявлении.

Ну возможно что это правильная логика.

Но без unsafeCoerce косяков бы не было ;-)

1) никто не говорил что его можно с GADT готовить;
2) даже если сделать unsafeCource не в ‘V1 a’, а в ‘(∀a.) a’, получается та же фигня.

> Чтобы отправлять сообщения в эту группу, отправьте письмо на электронный адрес haskell...@googlegroups.com.
> Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/haskell-russian/CAO-1Pb49-f2UP9Aoc%2BSPYhhOmEbuC%2BJJA4ZACSVOB7B%3DTTKcjA%40mail.gmail.com.
> Чтобы настроить другие параметры, перейдите по ссылке https://groups.google.com/d/optout.

[Alexander V Vershilov]

2014-07-30 19:56 GMT+04:00 Antonio Nikishaev <anto...@gmail.com>:
>
> On 30 Jul 2014, at 18:08, Alexander V Vershilov <alexander...@gmail.com> wrote:
>
>> Не могли бы вы немного распространить ответ?
>
>> Просто иначе - в случае если тип выводится, как V1 GHC.Prim.Any делать честный матчинг по всем конструкторам указанным в case, даже в том случае, если там есть полиморфные типы то выбирать тот, у которого конструктор подходит, а не первый подходящий при объявлении.
>
> Ну возможно что это правильная логика.
>
> Но без unsafeCoerce косяков бы не было ;-)
>
> 1) никто не говорил что его можно с GADT готовить;
> 2) даже если сделать unsafeCource не в ‘V1 a’, а в ‘(∀a.) a’, получается та же фигня.

Не могли бы вы подкрепить это утверждение какими-либо ссылками на документацию,
или хотя бы расписать подробнее.

Дело в том, что:

0. unsafeCorce тут в общем-то ни при чем, хотя внимание отвлекает

1. проблема есть только в полиморфном случае, во всех остальных
случаях данный код работает верно.

2. обоснование для core генерируемого при компиляции найти крайне сложно

3. в ghc-HEAD это поведение исправлено и везде ожидаемый результат.

Поэтому мне сложно понять, почему утверждения 1 и 2 и утверждение про
unsafeCoerce
верны..

> Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/9D420666-AF3A-405C-A143-0BD673206E0A%40gmail.com.

> Настройки подписки и доставки писем: https://groups.google.com/d/optout.



--

Alexander

[Alexander V Vershilov]

По поводу:

> Ну тип-то у него получается ‘V1 a’. Как иначе?

вот, пример, использования полиморфного GADT:


test4 :: V1 a -> String
test4 x = case x of
V1A a -> show a
V1B b -> show b
V1a c -> show c

Если тип выводится как `V1 a` и ситуация та же, то логичнопредположить



2014-07-30 20:05 GMT+04:00 Alexander V Vershilov
<alexander...@gmail.com>:

--
Alexander

[Alexander V Vershilov]

извиняюсь, не дописал, то логично предположить аналогичное поведение,
однако мы видим следующее:

*Main> test4 (V1A 1)
"1"
*Main> test4 (V1B 1)
"1.0"
*Main> test4 (V1a ())
"()"

можно предположить, что тут честно выводится мономорфный тип, но:

*Main> test4 (unsafeCoerce (V1A 1) :: V1 a )
"1"
*Main> test4 (unsafeCoerce (V1B 1.0) :: V1 a )
"1.0"

демонстрирует другое поведение.

--
Alexander

[Maxim Taldykin]

Мне кажется, проблема действительно где-то в районе viewV0, viewV1.

Какую реализацию может иметь функция с типом `S a -> V0 a`?

Для V0 у нас есть только undefined и два конструктора 

    V0A :: Int -> V0 A

    V0B :: Double -> V0 B

Конструкторы не подходят: если, например, вернуть V0A, то функция при подстановке `B` вместо `a` перестанет работать.

Остаётся только undefined.

Если вы придумываете такой функции какую-то семантику и форсируете её с помощью `unsafeCoerce`, то вполне ожидаемо, что undefined behavior поджидает вас за углом.

А вот для типа `S a -> V1 a`  кроме undefined подходит реализация `V1a ()`.

Исходя из этого можно интерпретировать результаты тестов:

  - test0 ничего не показывает, потому как ни один из кейсов не может быть результатом `viewV0 s :: V0 a`;

  - test1 работает нормально, потому как тут мономорфный тип;

  - в test2 срабатывает последний кейс, потому как кроме `V1a ()` ничего другого честный `viewV1 s :: V1 a` вернуть не может.

Не ясно только почему компилятор не ругается матерно.

30 июля 2014 г., 20:17 пользователь Alexander V Vershilov <alexander...@gmail.com> написал:

Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/CAO-1Pb4hDEuSHHeH%3DUwmMRu8AjU25GHUG2dHKroE5zp4P-_zMw%40mail.gmail.com.

[Alexander V Vershilov]

Ну тут на самом деле оказалось несколько проблем. Попробую расписать
их, а потом задать
вопросы по ответу, т.к. я не все понял.

Проблема №1. В общем-то с точки зрения программы самая серьёзная, но
её исправление
скрывает остальные.

Тип фунции cast принципиально не верен

> cast :: M -> SomeS -> S a

Дело в том, что `S a` выводится из того, как значение используется, и
не зависит от входных
параметров, в итоге возможны варианты:

a. cast A s :: S A -- так должно работать на самом деле
b. cast A s :: S a -- тут тип более полиморфный, чем на самом деле,
это в общем-то неверно,
но в случае с V не страшно
c. cast A s :: S B -- принципиально неверно

В данном случае решением было использование синглтонов для типа M и
изменение типа
cast на

> cast :: SM a -> SomeS -> S a

теперь случаи b и с невозможны. Собственно в проекте этот вариант
теперь используется,
но вопрос по другим проблемам остался.

Проблема №2. генерация кода.

Я вижу 2 адекватных варианта поведения ghc, в коде приведенном вначале:
1. typechecker не примет программу
2. typechecker принимает программу и тогда в case производится матчинг
по конструкторам GADT

поскольку код `case (x :: V1 a) of { V1A -> ... ; V1B -> ...; V1a ->
...}` валиден, и case будет
проверять все конструкторы, то вариант 2. представляется вполне логичным.

Про viewV0:

Если мы ограничены undefined и констукруторами, то сделать логичный
view тяжеловато,
но в данном случае у меня есть функция `typeOf :: S a -> M`, которая
возвращает тип, и
благодаря этой функции я могу написать правильный view. Правда у
компилятора нету информации
об этом.

Проблема №3. генерация кода

Ещё более инетерсное поведение наблюдается если добавть ещё один
конструктор с полиморфным
типом, в этом случае `case` выберет ветку с полиморфным конструктором,
который объявлен первым
при декларации типа, т.е.

data V2 :: m -> * where
V2A :: Int -> V2 A
V2B :: Double -> V2 B
V2a :: () -> V2 a
V2b :: () -> V2 b

case (viewV2 s) of
V2A -> 1
V2B -> 2
V2b -> 3
V2a -> 4

результат будет '4', что совсем уж неочевидно.

> https://groups.google.com/d/msgid/haskell-russian/CABxyK-nE3AMOQBdX4thTagufVNSkwwCpgNEKfonMgG2wNiMqOQ%40mail.gmail.com.

>
> Чтобы настроить другие параметры, перейдите по ссылке
> https://groups.google.com/d/optout.



--

Alexander

[Maxim Taldykin]

31 июля 2014 г., 10:56 пользователь Alexander V Vershilov <alexander...@gmail.com> написал:

Тип фунции cast принципиально не верен

> cast :: M -> SomeS -> S a

Скорее не верен

data SomeS = forall a . SomeS (S a)

После `SomeS (S 2 :: S A)` типовый тег `A` исчезает навсегда и бесследно. Чтобы сохранить информацию о нём, нужно `a` ограничить каким-нибудь классом.

 

В данном случае решением было использование синглтонов для типа M и
изменение типа
cast на

> cast :: SM a -> SomeS -> S a

теперь случаи b и с невозможны. Собственно в проекте этот вариант
теперь используется,

Зато возможен случай `cast A (SomeS (S 2 :: S B)) :: S A`.

 

Про viewV0:

Если мы ограничены undefined и констукруторами, то сделать логичный
view тяжеловато,
но в данном случае у меня есть функция `typeOf :: S a -> M`, которая
возвращает тип, и
благодаря этой функции я могу написать правильный view. Правда у
компилятора нету информации
об этом.

У компилятора действительно нет этой информации, потому как typeOf возвращает не тип, а значение типа М. То, что есть ещё и kind с таким же названием, это просто случайность. Без синглтонов они никак не связаны.

Единственность реализации `viewV0 = undefined` следует примерно из Reynolds's parametricity theorem (я не знаю как она формулируется).

`typeOf :: S a -> M` никак не поможет получить значение типа `V0 a`, потому как она про V0 ничего не знает.

 

[Alexander V Vershilov]

> Скорее не верен

> data SomeS = forall a . SomeS (S a)

нет, это точно верно.

как написано в комментариях SomeS обозначает, что тег 'a' неизвестен
на момент компиляции (в целом, все S, которые приходят из внешней
библиотеки завернуты в SomeS, который нам принципиально незвестен),
поэтому хранить
нечего, а хранить Any - принципиально неверно.

Для того, чтобы получить 'a', который мы ожидаем и используется метод
'cast', который

а). в runtime проверит, что тип действительно соответсвует тегу,
который мы хотим проставить
и кинет error в противном случае

б). проставит тег 'a'.

> Зато возможен случай `cast A (SomeS (S 2 :: S B)) :: S A`.

который вернёт _|_, и это вполне нормально. В принципе, можно добавить
безопасный вариант `safeCast :: SM a -> SomeS -> Maybe (S a)`, но мне кажется,
что это ортогонально проблеме.

> Единственность реализации `viewV0 = undefined` следует примерно из
> Reynolds's parametricity theorem (я не знаю как она формулируется).

Cпасибо, поищу.

> `typeOf :: S a -> M` никак не поможет получить значение типа `V0 a`,
> потому как она про V0 ничего не знает.

Совсем не понял утверждения, `typeOf` не должна ничего знать о `V`,
typeOf служит для того, чтобы в runtime узнать значение 'a', которым
протегировано 'S'.

На всякий случай переформулирую моё утверждение.
Пусть есть типы `S (a::M)` и `V (a::M)` тогда при наличии функции
`typeOf :: S a -> M`, мы можем записать `view :: S a -> V a`, такую, что для
каждого S протегированного конкретного тегом 'a', она вернёт V протегированный
тем же тегом.
В данном случае моё ожидание заключается в следующем, если S a - полиморфный,
то значит мы не можем знать, что тип view является V a, посколько V A
и V B, тоже
попадают в V a, то нужно проверять все конструкторы.

> --
> Вы получили это сообщение, поскольку подписаны на группу "Русский Haskell".
> Чтобы отменить подписку на эту группу и больше не получать от нее сообщения,
> отправьте письмо на электронный адрес
> haskell-russi...@googlegroups.com.
> Чтобы отправлять сообщения в эту группу, отправьте письмо на электронный
> адрес haskell...@googlegroups.com.
> Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке

> https://groups.google.com/d/msgid/haskell-russian/CABxyK-%3D3n1TxoUAvBFugnCBzG%3Dhxr4swU4R4Gkei6eN9a956rw%40mail.gmail.com.

[Maxim Taldykin]

31 июля 2014 г., 12:29 пользователь Alexander V Vershilov <alexander...@gmail.com> написал:

> Скорее не верен

> data SomeS = forall a . SomeS (S a)

нет, это точно верно.

как написано в комментариях SomeS обозначает, что тег 'a' неизвестен
на момент компиляции (в целом, все S, которые приходят из внешней
библиотеки завернуты в SomeS, который нам принципиально незвестен),
поэтому хранить
нечего, а хранить Any - принципиально неверно.

SomeS кладёт `S a` в коробочку из которой никак невозможно что-нибудь узнать про `a`. Если бы `a` был ограничен каким-то классом то из этой коробочки торчал бы проводок, по которому можно что-то узнать про этот `a`.

Я не могу быстро придумать примера в котором был бы полезен existential без ограничений.

 

Для того, чтобы получить 'a', который мы ожидаем и используется метод
'cast', который

а). в runtime проверит, что тип действительно соответсвует тегу,
который мы хотим проставить
и кинет error в противном случае

**В рантайме нет никаких типов.**

Если вы хотите типов в рантайме, используйте Dynamic (который на самом деле и есть existential ограниченный классом Typeable).

 

> Единственность реализации `viewV0 = undefined` следует примерно из
> Reynolds's parametricity theorem (я не знаю как она формулируется).

Cпасибо, поищу.

Про неё Wadler пишет в "Theorems for Free!".

 

> `typeOf :: S a -> M` никак не поможет получить значение типа `V0 a`,
> потому как она про V0 ничего не знает.

Совсем не понял утверждения, `typeOf` не должна ничего знать о `V`,
typeOf служит для того, чтобы в runtime узнать значение 'a', которым
протегировано 'S'.

На всякий случай переформулирую моё утверждение.
Пусть есть типы `S (a::M)` и `V (a::M)` тогда при наличии функции
`typeOf :: S a -> M`, мы можем записать `view :: S a -> V a`, такую, что для
каждого S протегированного конкретного тегом 'a', она вернёт V протегированный
тем же тегом.

Для типа V0 это утверждение неверно.

В данном случае моё ожидание заключается в следующем, если S a - полиморфный,
то значит мы не можем знать, что тип view является V a, посколько V A
и V B, тоже
попадают в V a, то нужно проверять все конструкторы.

GHC считает наоборот, поэтому test0 из вашего первого письма ничего не выводит и вообще никаких кейсов не проверяет.

(Не удивлюсь, если при должных гарантиях строгости и с флагом -O2 он превращается в `return ()`).

Чтобы добавлять сообщения в эту группу, отправьте письмо по адресу haskell...@googlegroups.com.

Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/CAO-1Pb67xS%2BdJNzLBHi19PQzV5JBmZUsH50zJhAtpa0QgPKi2w%40mail.gmail.com.

[Alexander V Vershilov]

2014-07-31 13:17 GMT+04:00 Maxim Taldykin <jor...@gmail.com>:
>
>
>
> 31 июля 2014 г., 12:29 пользователь Alexander V Vershilov
> <alexander...@gmail.com> написал:
>
>> > Скорее не верен
>>
>> > data SomeS = forall a . SomeS (S a)
>>
>> нет, это точно верно.
>>
>> как написано в комментариях SomeS обозначает, что тег 'a' неизвестен
>> на момент компиляции (в целом, все S, которые приходят из внешней
>> библиотеки завернуты в SomeS, который нам принципиально незвестен),
>> поэтому хранить
>> нечего, а хранить Any - принципиально неверно.
>
>
> SomeS кладёт `S a` в коробочку из которой никак невозможно что-нибудь узнать
> про `a`.

SomeS служит для того, чтобы сделать так чтобы было принципиально невозможно
узнать про `a`. Т.к. про него ничего не известно, пример использования

foreignCall :: IO SomeS - тут мы не знаем, какой S есть, и _единственное_
валидное средство это использование `cast`

> Если бы `a` был ограничен каким-то классом то из этой коробочки
> торчал бы проводок, по которому можно что-то узнать про этот `a`.
> Я не могу быстро придумать примера в котором был бы полезен existential без
> ограничений.

Пример перед вами.

>>
>>
>> Для того, чтобы получить 'a', который мы ожидаем и используется метод
>> 'cast', который
>>
>> а). в runtime проверит, что тип действительно соответсвует тегу,
>> который мы хотим проставить
>> и кинет error в противном случае
>
>
> **В рантайме нет никаких типов.**

Это не верное в общем случае утверждение, и конкретно в данном.

> Если вы хотите типов в рантайме, используйте Dynamic (который на самом деле
> и есть existential ограниченный классом Typeable).

Я очередной раз пишу, что S это указатель на внешние сишные структуры, в
них хранится информация о том, какого они типа. Dymanic и Typeable тут будут
излишни и более того в большинстве случаев неверны.

В упрощенном варианте, используемом тут, информация о типе хранится в
четности значения.

>> > Единственность реализации `viewV0 = undefined` следует примерно из
>> > Reynolds's parametricity theorem (я не знаю как она формулируется).
>>
>> Cпасибо, поищу.
>
>
> Про неё Wadler пишет в "Theorems for Free!".
>
>>
>> > `typeOf :: S a -> M` никак не поможет получить значение типа `V0 a`,
>> > потому как она про V0 ничего не знает.
>>
>> Совсем не понял утверждения, `typeOf` не должна ничего знать о `V`,
>> typeOf служит для того, чтобы в runtime узнать значение 'a', которым
>> протегировано 'S'.
>>
>> На всякий случай переформулирую моё утверждение.
>> Пусть есть типы `S (a::M)` и `V (a::M)` тогда при наличии функции
>> `typeOf :: S a -> M`, мы можем записать `view :: S a -> V a`, такую, что
>> для
>> каждого S протегированного конкретного тегом 'a', она вернёт V
>> протегированный
>> тем же тегом.
>
>
> Для типа V0 это утверждение неверно.

контр-пример?

>> В данном случае моё ожидание заключается в следующем, если S a -
>> полиморфный,
>> то значит мы не можем знать, что тип view является V a, посколько V A
>> и V B, тоже
>> попадают в V a, то нужно проверять все конструкторы.
>
>
> GHC считает наоборот, поэтому test0 из вашего первого письма ничего не
> выводит и вообще никаких кейсов не проверяет.
> (Не удивлюсь, если при должных гарантиях строгости и с флагом -O2 он
> превращается в `return ()`).

Как я уже писал это исправлено в GHC-HEAD поэтому данная аргументация
неприменима. Как впрочем и вообще отсылка к поведению компилятора в
случае вопроса о том, правильное ли поведение у компилятора в данном
случае.

> https://groups.google.com/d/msgid/haskell-russian/CABxyK-kacz%3Db6UeaDizYQum4MjA9guS5RVSqL0HHkYeNe8KNxQ%40mail.gmail.com.

[Maxim Taldykin]

31 июля 2014 г., 13:44 пользователь Alexander V Vershilov <alexander...@gmail.com> написал:

2014-07-31 13:17 GMT+04:00 Maxim Taldykin <jor...@gmail.com>:

SomeS служит для того, чтобы сделать так чтобы было принципиально невозможно
узнать про `a`. Т.к. про него ничего не известно, пример использования

foreignCall :: IO SomeS - тут мы не знаем, какой S есть, и _единственное_
валидное средство это использование `cast`

Да, только если cast вот такой:

data SomeS = forall a . Castable a => SomeS (S a)

class Castable a where typeOf :: S a -> M

instance Castable A where typeOf _ = A

instance Castable B where typeOf _ = B

cast :: Castable a => M -> SomeS -> Maybe (S a)

cast a s@(SomeS (S i))

    | typeOf s == a = Just (S i)

    | otherwise = Nothing

> **В рантайме нет никаких типов.**

Это не верное в общем случае утверждение, и конкретно в данном.

Т.е. в скомпилированной программе есть какие-то сведения о том, что `SomeS (S 123 :: S A)` имеет какое-то отношение к A?

 

>> Пусть есть типы `S (a::M)` и `V (a::M)` тогда при наличии функции
>> `typeOf :: S a -> M`, мы можем записать `view :: S a -> V a`, такую, что
>> для
>> каждого S протегированного конкретного тегом 'a', она вернёт V
>> протегированный
>> тем же тегом.
>
>
> Для типа V0 это утверждение неверно.

контр-пример?

Контрпримером являются результаты ваших тестов.

Вы попробовали сделать функцию с таким типом и реализацией отличной от undefined и получили неожиданное поведение.

 

>> В данном случае моё ожидание заключается в следующем, если S a -
>> полиморфный,
>> то значит мы не можем знать, что тип view является V a, посколько V A
>> и V B, тоже
>> попадают в V a, то нужно проверять все конструкторы.
>
>
> GHC считает наоборот, поэтому test0 из вашего первого письма ничего не
> выводит и вообще никаких кейсов не проверяет.
> (Не удивлюсь, если при должных гарантиях строгости и с флагом -O2 он
> превращается в `return ()`).

Как я уже писал это исправлено в GHC-HEAD поэтому данная аргументация
неприменима. Как впрочем и вообще отсылка к поведению компилятора в
случае вопроса о том, правильное ли поведение у компилятора в данном
случае.

Ок, это и в обратную сторону тоже верно. Если в GHC-HEAD работает, это ещё не значит, что так и должно быть.

Мне кажется, что вам удалось обмануть компилятор (с помощью unsafeCoerce), а он вам за это undefined behavior.

[Antonio Nikishaev]

0) unsafeCoerce тут очень при чём. Без него никакого цирка не получится.

1) Притянуто за уши, но: раз у unsafeCoerce# не указаны gadt'ы, значит не положено (ну почему бы и не так :).

2) просто: заменяем тип view на S a → b. Получаем ту же фиговину.

Надо посмотреть внимательнее, но я так сразу ticket# не вижу который это исправил.

> Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/CAO-1Pb68XfzOdegkfs6O_aS2d3tdxp6CiJkEsLn2wsA93zw3-A%40mail.gmail.com.

[Alexander V Vershilov]

2014-07-31 14:29 GMT+04:00 Maxim Taldykin <jor...@gmail.com>:
>
>
>
> 31 июля 2014 г., 13:44 пользователь Alexander V Vershilov
> <alexander...@gmail.com> написал:
>>
>> 2014-07-31 13:17 GMT+04:00 Maxim Taldykin <jor...@gmail.com>:
>>
>> SomeS служит для того, чтобы сделать так чтобы было принципиально
>> невозможно
>> узнать про `a`. Т.к. про него ничего не известно, пример использования
>>
>> foreignCall :: IO SomeS - тут мы не знаем, какой S есть, и _единственное_
>> валидное средство это использование `cast`
>
>
> Да, только если cast вот такой:
>
> data SomeS = forall a . Castable a => SomeS (S a)
> class Castable a where typeOf :: S a -> M
> instance Castable A where typeOf _ = A
> instance Castable B where typeOf _ = B
>
> cast :: Castable a => M -> SomeS -> Maybe (S a)
> cast a s@(SomeS (S i))
> | typeOf s == a = Just (S i)
> | otherwise = Nothing

Ещё раз, пожалуйста прочитайте, что такое S в программе.

>> > **В рантайме нет никаких типов.**
>>
>> Это не верное в общем случае утверждение, и конкретно в данном.
>
>
> Т.е. в скомпилированной программе есть какие-то сведения о том, что `SomeS
> (S 123 :: S A)` имеет какое-то отношение к A?

Да, т.к. S это указатель на сишную структуру данных состоящую из нескольких
полей, одно из который это тип выдажения, который имеет однозначное отображение
в тип M. Таким образом, S имеет информацию об A.
Ещё раз подчерну информация о типе хранится в сишной структуре, отображение
её в систему типов haskell это упрощение и добавление безопасности для некоторых
юзкейсов.

>> >> Пусть есть типы `S (a::M)` и `V (a::M)` тогда при наличии функции
>> >> `typeOf :: S a -> M`, мы можем записать `view :: S a -> V a`, такую,
>> >> что
>> >> для
>> >> каждого S протегированного конкретного тегом 'a', она вернёт V
>> >> протегированный
>> >> тем же тегом.
>> >
>> >
>> > Для типа V0 это утверждение неверно.
>>
>> контр-пример?
>
>
> Контрпримером являются результаты ваших тестов.

В том и только том случае, если реализация правильная, учитывая, что у разных
GHC разное поведение, вопрос о правильности реализации под сомнением.

Если же у вас нету сомнений по поводу правильности результата, то можете ли
вы прокомментировать результат следующего теста, который по моему мнению
ни объясняется тем, что вы описали выше, ни любым другим разумным способом:

data V1 :: M -> * where
V1A :: Int -> V1 A
V1B :: Double -> V1 B
V1a :: () -> V1 a

V1b :: () -> V1 a

test5 :: IO ()
test5 =

let s = cast A (SomeS (S 4))
in case viewV1 s of

V1A{} -> putStrLn "1"
V1B{} -> putStrLn "2"
V1b{} -> putStrLn "3"
V1a{} -> putStrLn "4"

Результатом выполнения данного кода будет "4", что заставляет засомневаться
логичности отсылок к результатам тестов.

> Вы попробовали сделать функцию с таким типом и реализацией отличной от
> undefined и получили неожиданное поведение.
>
>>
>>
>> >> В данном случае моё ожидание заключается в следующем, если S a -
>> >> полиморфный,
>> >> то значит мы не можем знать, что тип view является V a, посколько V A
>> >> и V B, тоже
>> >> попадают в V a, то нужно проверять все конструкторы.
>> >
>> >
>> > GHC считает наоборот, поэтому test0 из вашего первого письма ничего не
>> > выводит и вообще никаких кейсов не проверяет.
>> > (Не удивлюсь, если при должных гарантиях строгости и с флагом -O2 он
>> > превращается в `return ()`).
>>
>> Как я уже писал это исправлено в GHC-HEAD поэтому данная аргументация
>> неприменима. Как впрочем и вообще отсылка к поведению компилятора в
>> случае вопроса о том, правильное ли поведение у компилятора в данном
>> случае.
>
>
> Ок, это и в обратную сторону тоже верно. Если в GHC-HEAD работает, это ещё
> не значит, что так и должно быть.

Ну собственно этот вопрос я тут поднял исключительно ради того, чтобы понять,
какая оптимизация позволяет так поступать с кодом. И указал это, для того, чтобы
не использовать результаты выполнения кода, как аргументацию к мнению.

> Мне кажется, что вам удалось обмануть компилятор (с помощью unsafeCoerce), а
> он вам за это undefined behavior.

возможно.


--
Alexander

[Antonio Nikishaev]

cast тут вообще не при чём


> main =
> case (unsafeCoerce (V1A 2)) of

> V1A{} -> putStrLn "test2 - A"
> V1B{} -> putStrLn "test2 - B"
> V1a{} -> putStrLn "test2 - O_o"

> --
> Вы получили это сообщение, поскольку подписаны на группу "Русский Haskell".
> Чтобы отменить подписку на эту группу и больше не получать от нее сообщения, отправьте письмо на электронный адрес haskell-russi...@googlegroups.com.
> Чтобы отправлять сообщения в эту группу, отправьте письмо на электронный адрес haskell...@googlegroups.com.

> Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/haskell-russian/CABxyK-mob310W22TMhgH0ypjhF19SNiUq-z9h1fC9JLuzzpudg%40mail.gmail.com.

[Maxim Taldykin]

31 июля 2014 г., 15:12 пользователь Alexander V Vershilov <alexander...@gmail.com> написал:

data V1 :: M -> * where
  V1A :: Int -> V1 A
  V1B :: Double -> V1 B
  V1a :: () -> V1 a

  V1b :: () -> V1 a

test5 :: IO ()
test5 =

  let s = cast A (SomeS (S 4))
  in case viewV1 s of

      V1A{} -> putStrLn "1"
      V1B{} -> putStrLn "2"
      V1b{} -> putStrLn "3"
      V1a{} -> putStrLn "4"

Результатом выполнения данного кода будет "4", что заставляет засомневаться
логичности отсылок к результатам тестов.

Рассуждения аналогичны случаю с test2.

Поскольку `viewV1 s` имеет тип `V1 a`, то результатом может быть либо `V1a x` либо `V1b x`. Исходя из этого, компилятор отбрасывает первые два кейса и оставляет последние два.

В рантайме в кейс внезапно приходит `V1A x`, и он от неожиданности возвращает первый попавшийся результат.

Т.е. можно предположить, что оптимизатор превращает кейс в:

    case xx of

        V1b _ -> putStrLn "3"

        _        -> putStrLn "4"

Хотя более логично было бы

    case xx of

        V1b _ -> putStrLn "3"

        V1a _ -> putStrLn "4"

        _        -> error "Unexpected V1"

Думаю, если в viewV1 вы поменяете V1A и V1B на V1a и V1b, всё будет работать ожидаемо.

[Alexander V Vershilov]

Всем спасибо за обсуждение. Указанные теоремы я обязательно почитаю
для общего развития.

В поднятом баге [1] simonpj расписал причину почему в ghc-7.8.3 поведение
было неверным, и почему исправлено в ghc-HEAD.

[1] https://ghc.haskell.org/trac/ghc/ticket/9380#comment:4

> Чтобы добавлять сообщения в эту группу, отправьте письмо по адресу haskell...@googlegroups.com.

> Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/FB3CADD4-ED84-470B-B1D0-FC1EEB2F3D0A%40gmail.com.

> Настройки подписки и доставки писем: https://groups.google.com/d/optout.



--

Alexander

[Maxim Taldykin]

31 июля 2014 г., 16:29 пользователь Alexander V Vershilov <alexander...@gmail.com> написал:

Всем спасибо за обсуждение. Указанные теоремы я обязательно почитаю
для общего развития.

В поднятом баге [1] simonpj расписал причину почему в ghc-7.8.3 поведение
было неверным, и почему исправлено в ghc-HEAD.

[1] https://ghc.haskell.org/trac/ghc/ticket/9380#comment:4

Вот только совсем не ясно почему раньше было неверно, а теперь верно.

По ссылке объяснение того как как оно работало раньше полностью совпадает с тем, что я только что писал.

 

Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/CAO-1Pb79aXeW3eNpZKha%2Br1MOF24yUBsSpBMcLLfd%3DRyeWvOzQ%40mail.gmail.com.

[Serguey Zefirov]

Что за хтонический ужас вызвал ты из преисподней?

У меня на ghc 7.6.3 test2 выдаёт "hit a CASEFAIL" в ghci.

Думаю, правы те, кто намекает на undefined behavior. Надо переписать проще.

30 июля 2014 г., 11:16 пользователь Alexander V Vershilov <alexander...@gmail.com> написал:

--
Alexander

--
Вы получили это сообщение, поскольку подписаны на группу Русский Haskell.

Чтобы отменить подписку на эту группу и больше не получать от нее сообщения, отправьте письмо на электронный адрес haskell-russi...@googlegroups.com.
Чтобы добавлять сообщения в эту группу, отправьте письмо по адресу haskell...@googlegroups.com.

Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/CAO-1Pb55UZHMu6uTcit_j56qktO9VxmcbZm2LftmUqULX1W0Dg%40mail.gmail.com.

[Maxim Taldykin]

31 июля 2014 г., 16:54 пользователь Serguey Zefirov <serg...@gmail.com> написал:

Что за хтонический ужас вызвал ты из преисподней?

У меня на ghc 7.6.3 test2 выдаёт "hit a CASEFAIL" в ghci.

Думаю, правы те, кто намекает на undefined behavior. Надо переписать проще.

Там не всё так просто. SPJ намекает на то, что это бага https://ghc.haskell.org/trac/ghc/ticket/9380#comment:4

Чтобы отправлять сообщения в эту группу, отправьте письмо на электронный адрес haskell...@googlegroups.com.

Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/haskell-russian/CABFQQ%3DD2ofS56iq1AVLqhZHNZ90Hr6x3H-2p4UvF_h0Y0Ehc9A%40mail.gmail.com.

[Alexander V Vershilov]

Нормальный хтонический ужас. CASEFAIL это т.к. при упрощении реального кейса
в помещающийся на странице я что-то переупростил (минимальный кейс
проверял только на 7.8),
т.к. с unsafeCoerce легко напороться на проблему выкинув лишнюю часть решения,
что было продемонстрировано в этом треде. А так все более мирно и
работает в т.ч.
на 7.6.

Проще оно, в принципе, переписывается (и была бы моя воля я бы переписал), но
тогда теряются полезные свойства конкретно этого решения.

> Чтобы отправлять сообщения в эту группу, отправьте письмо на электронный
> адрес haskell...@googlegroups.com.
> Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке
> https://groups.google.com/d/msgid/haskell-russian/CABFQQ%3DD2ofS56iq1AVLqhZHNZ90Hr6x3H-2p4UvF_h0Y0Ehc9A%40mail.gmail.com.
>
> Чтобы настроить другие параметры, перейдите по ссылке
> https://groups.google.com/d/optout.

--
Alexander

[Maxim Taldykin]

Вот есть такой более минимальный пример:

{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}

import Unsafe.Coerce

data X = A | B

data Y (x :: X) where

  YA   :: Char   -> Y A

  YB   :: Int    -> Y B

  Yany :: String -> Y x

view :: Y a -> Y b

view = unsafeCoerce

main :: IO ()

main = case view $ YA 'a' of

  YA   x -> print x

  YB   x -> print x

  Yany x -> print x

На GHC <= 7.8 он выкинет segmentation fault. На GHC-HEAD он напечатает 'a'.

Будете смеяться, но я всё ещё считаю, что исходное поведение более верное (за исключением того, можно человеческую ошибку писать, а не сегфолтиться).

У меня единственный аргумент: параметрический полиморфизм позволяет компилятору заключить, что результатом `view (YA 'a')` может быть только `Yany` (или _|_). Поэтому компилятор вправе выкинуть из кейса сравнение с YA и YB.

31 июля 2014 г., 17:13 пользователь Alexander V Vershilov <alexander...@gmail.com> написал:

Просмотреть это обсуждение в Сети можно по адресу https://groups.google.com/d/msgid/haskell-russian/CAO-1Pb7he%3DrL%2BP12ySzgKJwiXaHE0DRpo9As%3Dk47A0P4pqCmPg%40mail.gmail.com.

[Alexander V Vershilov]

Не-не-не, unsafeCoerce в моём коде и в этом использовался в несколько разных
случаях, и в то время как тут это действительно небезопасно и должно
вести к проблеме
в моём случае все было хорошо.

> У меня единственный аргумент: параметрический полиморфизм позволяет компилятору заключить,
> что результатом `view (YA 'a')` может быть только `Yany` (или _|_).
> Поэтому компилятор вправе выкинуть из кейса сравнение с YA и YB.

тут в общем то такой вопрос, являются ли YA или YB элементами типа Y a.
ответ на который должен определять поведения компилятора.

> https://groups.google.com/d/msgid/haskell-russian/CABxyK-nZYHFS6kAmdSJ-cQYKNn3OmzEJXWPokveodWrCyjyUmQ%40mail.gmail.com.