Size: a a a

2021 January 21

к

кана in Haskell Start
но это все отвечает на вопрос как устроены gadts, но слабо отвечает, для чего
источник

AN

Absolute Nikola in Haskell Start
data X a
 = (a ~ String) => A Int
 | (a ~ Int) => B String

Т.е вот здесь, когда мы создаем тип X при помощи конструктора А мы вместе со значением таскаем еще знание что у X параметр String ?
источник

к

кана in Haskell Start
тут классический пример это типизированное AST

data Expr a where
 LitInt :: Int -> Expr Int
 LitBool :: Bool -> Expr Bool
 Plus :: Expr Int -> Expr Int -> Expr Int
 And :: Expr Bool -> Expr Bool -> Expr Bool
 If :: Expr Bool -> Expr a -> Expr a -> Expr a
 Eq :: Expr a -> Expr a -> Expr Bool

если без If и Eq, такое семейство можно сделать и просто двумя типами, но If их склеивает
источник

к

кана in Haskell Start
Absolute Nikola
data X a
 = (a ~ String) => A Int
 | (a ~ Int) => B String

Т.е вот здесь, когда мы создаем тип X при помощи конструктора А мы вместе со значением таскаем еще знание что у X параметр String ?
да, вместе c A мы таскаем
1) число
2) пруф что a это String
пруф скорее всего стирается при компиляции после Core, это все нужно только для того чтобы вписаться в тайпчек
источник

к

кана in Haskell Start
кана
есть еще один способ смотреть на то что такое GADTs - посмотреть сначала на type families, а конкретно на data families, увидеть что нет закрытых дата тайпфемелис, и можно прийти к тому, что gadts это просто закрытые дата-семейства, только с другим синтаксисом (конкретно в хаскеле)

но конечно не совсем, полиморфные конструкторы в эту схему красиво не вписываются

в любом случае gadts разбивают один тип на семейство типов, где индекс - это те типы, которые матчатся в разных конструкторах
если бы для гадтов был бы синтаксис схожий с семействами, это бы выглядело как-то так

ВНИМАНИЕ НЕВАЛИДНЫЙ СИНТАКСИС

data family Expr a where
 Expr Int = LitInt Int | Plus (Expr Int) (Expr Int)
 Expr Bool = LitBool Bool | And (Expr Bool) (Expr Bool) | forall a. Eq (Expr a) (Expr a)
 Expr a = If (Expr Bool) (Expr a) (Expr a)
источник

JS

Jerzy Syrowiecki in Haskell Start
кана
если бы для гадтов был бы синтаксис схожий с семействами, это бы выглядело как-то так

ВНИМАНИЕ НЕВАЛИДНЫЙ СИНТАКСИС

data family Expr a where
 Expr Int = LitInt Int | Plus (Expr Int) (Expr Int)
 Expr Bool = LitBool Bool | And (Expr Bool) (Expr Bool) | forall a. Eq (Expr a) (Expr a)
 Expr a = If (Expr Bool) (Expr a) (Expr a)
простите, что влезаю, не разобравшись, но там же зависимость в другую сторону. тип зависит от конструктора, а не наоборот

это теоретически можно записать таким синтаксисом, но будет только хуже
источник

AN

Absolute Nikola in Haskell Start
кана
тут классический пример это типизированное AST

data Expr a where
 LitInt :: Int -> Expr Int
 LitBool :: Bool -> Expr Bool
 Plus :: Expr Int -> Expr Int -> Expr Int
 And :: Expr Bool -> Expr Bool -> Expr Bool
 If :: Expr Bool -> Expr a -> Expr a -> Expr a
 Eq :: Expr a -> Expr a -> Expr Bool

если без If и Eq, такое семейство можно сделать и просто двумя типами, но If их склеивает
вот это вот расскрывается в
data Expr a
 = (a ~ Int)  => LitInt Int
 | (a ~ Bool) => LitBool Bool
 | (a ~ Int)  => Plus (Expr Int) (Expr Int)
 | (a ~ Bool) => And (Expr Bool) (Expr Bool)
 | (a ~ a)    => If (Expr Bool) (Expr a) (Expr a)
 | (a ~ Bool) => Eq (Expr a) (Expr a) (Expr Bool)

?
источник

к

кана in Haskell Start
Jerzy Syrowiecki
простите, что влезаю, не разобравшись, но там же зависимость в другую сторону. тип зависит от конструктора, а не наоборот

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

из-за того что семейство закрытое, это работает в обе стороны

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

к

кана in Haskell Start
Absolute Nikola
вот это вот расскрывается в
data Expr a
 = (a ~ Int)  => LitInt Int
 | (a ~ Bool) => LitBool Bool
 | (a ~ Int)  => Plus (Expr Int) (Expr Int)
 | (a ~ Bool) => And (Expr Bool) (Expr Bool)
 | (a ~ a)    => If (Expr Bool) (Expr a) (Expr a)
 | (a ~ Bool) => Eq (Expr a) (Expr a) (Expr Bool)

?
| If (Expr Bool) (Expr a) (Expr a)
источник

JS

Jerzy Syrowiecki in Haskell Start
кана
это и практически так записывают в некоторых языках

из-за того что семейство закрытое, это работает в обе стороны

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

к

кана in Haskell Start
да, тип не определяет конструктор, он определяет множество конструкторов, биекции там нет
источник

JS

Jerzy Syrowiecki in Haskell Start
кана
да, тип не определяет конструктор, он определяет множество конструкторов, биекции там нет
я имел в виду, что ограничение типа GADT не сужает это множество, в отличие от data family, поэтому это принципиально разные вещи
источник

JS

Jerzy Syrowiecki in Haskell Start
кана
это и практически так записывают в некоторых языках

из-за того что семейство закрытое, это работает в обе стороны

мы спокойно не получаем ворнинг, когда только возможные конструкторы
или хочется иметь закрытые data family? но тогда это тоже не GADT
источник

к

кана in Haskell Start
как раз таки сужает, иначе повторюсь, где ворнинг при коде

data X a where
 A :: X Int
 B :: X String

f :: X Int -> Int
f A = 0
источник

JS

Jerzy Syrowiecki in Haskell Start
кана
как раз таки сужает, иначе повторюсь, где ворнинг при коде

data X a where
 A :: X Int
 B :: X String

f :: X Int -> Int
f A = 0
это примитивный пример. чуть усложним:

data Eizer a b where
 LeftInt :: Eizer Int b
 RightString :: Eizer a String

f :: Eizer Int b -> Int
f LeftInt = 0

a.hs:9:1-13: warning: [-Wincomplete-patterns]
   Pattern match(es) are non-exhaustive
   In an equation for ‘f’: Patterns not matched: RightString
 |
9 | f LeftInt = 0
 | ^^^^^^^^^^^^^
источник

к

кана in Haskell Start
потому что тут и подходят оба конструктора
источник

JS

Jerzy Syrowiecki in Haskell Start
вот и я о том же. c GADT так можно, а с DF нельзя
источник

JS

Jerzy Syrowiecki in Haskell Start
DF не разрешает пересекающиеся множества конструкторов, поэтому функциональный синтаксис естественен
источник

JS

Jerzy Syrowiecki in Haskell Start
GADT разрешает пересекающиеся множества конструкторов, поэтому функциональный синтаксис противоестественен
источник

к

кана in Haskell Start
с открытым нельзя

с открытыми тайп-семействами тоже нельзя

type family F a
type instance F Int = Int
type instance F a = String

а закрытость меняет правила
источник