Size: a a a

2021 January 21

AP

Aleksei (astynax) Pi... in Haskell Start
И ограничить эти типы при необходимости
источник

AP

Aleksei (astynax) Pi... in Haskell Start
data SorR a where
 Showable :: Show a => a -> SorR a
 Readable :: Read a => a -> SorR a

пример
источник

AP

Aleksei (astynax) Pi... in Haskell Start
тут вроде как и полиморфизм, но конструкторы имеют разные ограничения
источник

к

кана in Haskell Start
даже не то что более точно

формально GADTы позволяют вместо со значениями хранить и отношения между типами

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

тут A конструктор хранит не только значение типа Int, но еще и факт что "a" = String, что потом используется при матчинге
источник

AN

Absolute Nikola in Haskell Start
т.е мы можем накладывать свои ограничения на конструкторы и иметь свой тип для каждого конструктора?
источник

AN

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

к

кана in Haskell Start
возможно лучше всего сначала ознакомиться с coercions, описывать гадты без синтаксиса, а потом уже взять gadts как сахар для этого

data X a
 = (a ~ String) => A Int
 | (a ~ Int) => B String

data SorR a
 = Show a => Showable a
 | Read a => Readable a
источник

AN

Absolute Nikola in Haskell Start
понял, сейчас почитаю
источник

A

Aragaer in Haskell Start
я как раз кидал сюда ссылку на "монаду Set", там один из вариантов это GADT с "если Ord, то Set, иначе List"
источник

A

Aragaer in Haskell Start
     data SetM a where
       SMOrd :: Ord a => S.Set a -> SetM a
       SMAny :: [a] -> SetM a
источник

к

кана in Haskell Start
не уверен что есть какая-нибудь литература про это кроме пейперов
(Safe Zero-cost Coercions for Haskell или nokinds, или https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf)
источник

AP

Aleksei (astynax) Pi... in Haskell Start
Стоит ещё различать "GADT syntax" и "GADTs"
источник

AP

Aleksei (astynax) Pi... in Haskell Start
Потому что первое — просто другой способ записи тех же ADT. При котором все конструкторы всегда конструируют один и тот же тип.
источник

AP

Aleksei (astynax) Pi... in Haskell Start
(у GADTs разные конструкторы дают разные подмножества типов)
источник

к

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

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

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

A

Aleksandr Khristenko in Haskell Start
еще позволяет делать экзистенциальные типы
источник

AN

Absolute Nikola in Haskell Start
кана
возможно лучше всего сначала ознакомиться с coercions, описывать гадты без синтаксиса, а потом уже взять gadts как сахар для этого

data X a
 = (a ~ String) => A Int
 | (a ~ Int) => B String

data SorR a
 = Show a => Showable a
 | Read a => Readable a
А я правильно понимаю что ~ позволяет сказать тайпчекеру, что a и String одно и тоже?
источник

AN

Absolute Nikola in Haskell Start
или это еще что-то сверху дает?
источник

к

кана in Haskell Start
это констрейнт, это просьба на пруф того что a ~ String

data X a = (a ~ Int) => Y

f :: X a -> a
f Y = (0 :: Int)

main = print (f Y)

вот тут функция f должа возвращать тип a, а она возвращает Int, почему это тайпчекается вообще?

выглядит все так, будто Y пустой, и мб в рантайме он действительно пустой, но на самом деле там лежит собственно инстанс этого равенства, то есть его пруф

таким образом когда мы пишем

f :: X a -> a
f Y = 0

мы на самом деле пишем

coe :: a ~ b -> a -> b
symm :: a ~ b -> b ~ a

f :: X a -> a
f (Y {c :: a ~ Int}) = coe (symm c :: Int ~ a) (0 :: Int) :: a

и типы сходятся
источник

AN

Absolute Nikola in Haskell Start
Спасибо большое, вроде понял)
источник