Имеется простая тайп фемили type family Conc (a :: [*])

Question

Имеется простая тайп фемили type family Conc (a :: [*])

(b :: [*]) = (r :: [*]) | r -> a b
type instance Conc a '[] = a
type instance Conc a (x ': xs) = x ': Conc a xs

Проблема заключается в том, что благодаря зависимости тайпчекер падает с

RHS of injective type family equation is a bare type variable
Conc a '[] = a

Что не удивительно, так как у нас нет никаких гарантий что тайпфемили тотальны, однако задача как раз и заключается в то, что нужно как-то построить Conc с пруфом что r зависит от a и b, это вообще возможно?

#haskell #programming #russian

0

07.07.2020