AP
И ограничить эти типы при необходимости
data SorR a where
Showable :: Show a => a -> SorR a
Readable :: Read a => a -> SorR a пример
Size: a a a
2021 January 21
AP
пример
AP
тут вроде как и полиморфизм, но конструкторы имеют разные ограничения
к
даже не то что более точно
формально GADTы позволяют вместо со значениями хранить и отношения между типами
data X a where
A :: Int -> X String
B :: String -> X Int
тут A конструктор хранит не только значение типа Int, но еще и факт что "a" = String, что потом используется при матчинге
формально GADTы позволяют вместо со значениями хранить и отношения между типами
data X a where
A :: Int -> X String
B :: String -> X Int
тут A конструктор хранит не только значение типа Int, но еще и факт что "a" = String, что потом используется при матчинге
AN
т.е мы можем накладывать свои ограничения на конструкторы и иметь свой тип для каждого конструктора?
AN
точнее не тип, а пометку что у нас после этого конструктора тип вот так параметризован
к
возможно лучше всего сначала ознакомиться с coercions, описывать гадты без синтаксиса, а потом уже взять gadts как сахар для этого
data X a
= (a ~ String) => A Int
| (a ~ Int) => B String
data SorR a
= Show a => Showable a
| Read a => Readable aAN
понял, сейчас почитаю
A
я как раз кидал сюда ссылку на "монаду Set", там один из вариантов это GADT с "если Ord, то Set, иначе List"
A
data SetM a where
SMOrd :: Ord a => S.Set a -> SetM a
SMAny :: [a] -> SetM a
к
не уверен что есть какая-нибудь литература про это кроме пейперов
(Safe Zero-cost Coercions for Haskell или nokinds, или https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf)
(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
Стоит ещё различать "GADT syntax" и "GADTs"
AP
Потому что первое — просто другой способ записи тех же ADT. При котором все конструкторы всегда конструируют один и тот же тип.
AP
(у GADTs разные конструкторы дают разные подмножества типов)
к
есть еще один способ смотреть на то что такое GADTs - посмотреть сначала на type families, а конкретно на data families, увидеть что нет закрытых дата тайпфемелис, и можно прийти к тому, что gadts это просто закрытые дата-семейства, только с другим синтаксисом (конкретно в хаскеле)
но конечно не совсем, полиморфные конструкторы в эту схему красиво не вписываются
в любом случае gadts разбивают один тип на семейство типов, где индекс - это те типы, которые матчатся в разных конструкторах
но конечно не совсем, полиморфные конструкторы в эту схему красиво не вписываются
в любом случае gadts разбивают один тип на семейство типов, где индекс - это те типы, которые матчатся в разных конструкторах
A
еще позволяет делать экзистенциальные типы
AN
возможно лучше всего сначала ознакомиться с 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
или это еще что-то сверху дает?
к
это констрейнт, это просьба на пруф того что 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
и типы сходятся
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
Спасибо большое, вроде понял)