Телеграмм чат группы haskellru страница 14805

Size: a a a

Haskell

1644 membersпожаловаться на группу

2020 November 28

Roman in Haskell

в 8.10.2

источник

01:15пожаловаться #1

кана in Haskell

в хаскеле тайплевел куда развитее термлевела

источник

01:15пожаловаться #2

кана in Haskell

data Sigma a b
  = forall (x :: a). MkSigma (b x)

type Even = Sigma N IsEven

data N = Z | S N

data IsEven (a :: N) where
  EvenZ :: IsEven Z
  EvenS :: IsEven n -> IsEven (S (S n))

источник

01:17пожаловаться #3

Roman in Haskell

а еще можно делать open data types на тайп-левеле вот таким способом:

data family TyVarRep (var :: TyNameRep kind) :: kind

data family TyAppRep (fun :: dom -> cod) (arg :: dom) :: cod

TyVarRep и TyAppRep — это по сути конструкторы типа, индексированного кайндом. Определены через data family, чтобы можно было вот эту индексацию заэнкодить (через финальное :: kind и :: cod в первом и втором случае соответственно). Можно добавлять и другие дата фемели, а обрабатывать эту всю красоту через open type family. Итого, экспрешн проблем для индексированных типов солвд

источник

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

Roman in Haskell

скоро я все это притащу в прод

источник

01:28пожаловаться #5

Roman in Haskell

(там пока только половина)

источник

01:28пожаловаться #6

кана in Haskell

кана

data Sigma a b
  = forall (x :: a). MkSigma (b x)

type Even = Sigma N IsEven

data N = Z | S N

data IsEven (a :: N) where
  EvenZ :: IsEven Z
  EvenS :: IsEven n -> IsEven (S (S n))