Телеграмм чат группы haskell

2021 January 21

к

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

AN

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

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

источник

22:24пожаловаться #2

к

кана 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 их склеивает

источник

22:25пожаловаться #3

к

кана 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, это все нужно только для того чтобы вписаться в тайпчек

источник

22:26пожаловаться #4

к

кана 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)

источник

22:30пожаловаться #5

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)

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

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

источник

22:38пожаловаться #6

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)

?

источник

22:38пожаловаться #7

к

кана in Haskell Start

Jerzy Syrowiecki

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

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

это и практически так записывают в некоторых языках

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

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

источник

22:40пожаловаться #8

к

кана 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)

источник

22:40пожаловаться #9

JS

Jerzy Syrowiecki in Haskell Start

кана

это и практически так записывают в некоторых языках

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

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

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

источник

22:41пожаловаться #10

к

кана in Haskell Start

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

источник

22:41пожаловаться #11

JS

Jerzy Syrowiecki in Haskell Start

кана

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

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

источник

22:42пожаловаться #12

JS

Jerzy Syrowiecki in Haskell Start

кана

это и практически так записывают в некоторых языках

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

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

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

источник

22:44пожаловаться #13

к

кана in Haskell Start

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

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

f :: X Int -> Int
f A = 0

источник

22:45пожаловаться #14

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
  | ^^^^^^^^^^^^^

источник

22:54пожаловаться #15

к

кана in Haskell Start

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

источник

22:55пожаловаться #16

JS

Jerzy Syrowiecki in Haskell Start

вот и я о том же. c GADT так можно, а с DF нельзя

источник

22:56пожаловаться #17

JS

Jerzy Syrowiecki in Haskell Start

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

источник

22:57пожаловаться #18

JS

Jerzy Syrowiecki in Haskell Start

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

источник

22:57пожаловаться #19

к

кана in Haskell Start

с открытым нельзя

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

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

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

источник

22:58пожаловаться #20