Обычные имена для конструкторов: Inl и Inr:
data Sum :: [*] -> * where
Inl :: a -> Sum (a : as) -- INject Left
Inr :: !(Sum as) -> Sum (a : as) -- INject Right
Дополнительная строгость в Inr является необязательной.Рассмотрим Either a b.Этот тип имеет значения undefined, Left undefined и Right undefined вместе со всеми остальными.Считайте ваш Variant [a, b].Это имеет undefined, Singleton undefined, Variant undefined и Variant (Singleton undefined).Существует одно дополнительное частично неопределенное значение, которое не возникает с Either.Строгость Inr сводит воедино Inr undefined и undefined.Это означает, что вы не можете иметь значение только с «частично известным» вариантом.Все аннотации строгости в следующем для "правильности"Они вытесняют основания в местах, где вы, вероятно, не хотите основания.
Теперь, подпись singleton, как указывает @rampion, имеет ошибку использования до определения.Это должно быть:
singleton :: forall a b.
(Not (bs == '[]) || a == b) ~ True =>
a -> Variant (b ': bs)
Но это не совсем так.Если a ~ b, отлично, это работает.Если нет, компилятор не сможет гарантировать, что a находится в bs, потому что вы не ограничены этим.Эта новая подпись все еще терпит неудачу.Для большей мощности, особенно для будущих определений, вам понадобится что-то вроде
-- Elem x xs has the structure of a Nat, but doubles as a proof that x is in xs
-- or: Elem x xs is the type of numbers n such that the nth element of xs is x
data Elem (x :: k) (xs :: [k]) where
Here :: Elem x (x : xs)
There :: !(Elem x xs) -> Elem x (y : xs) -- strictness optional
-- boilerplate; use singletons or similar to dodge this mechanical tedium
-- EDIT: singletons doesn't support GADTs just yet, so this must be handwritten
-- See https://github.com/goldfirere/singletons/issues/150
data SElem x xs (e :: Elem x xs) where
SHere :: SElem x (x : xs) Here
SThere :: SElem x xs e -> SElem x (y : xs) (There e)
class KElem x xs (e :: Elem x xs) | e -> x xs where kElem :: SElem x xs e
instance KElem x (x : xs) Here where kElem = SHere
instance KElem x xs e => KElem x (y : xs) (There e) where kElem = SThere kElem
demoteElem :: SElem x xs e -> Elem x xs
demoteElem SHere = Here
demoteElem (SThere e) = There (demoteElem e)
-- inj puts a value into a Sum at the given index
inj :: Elem t ts -> t -> Sum ts
inj Here x = Inl x
inj (There e) x = Inr $ inj e x
-- try to find the first index where x occurs in xs
type family FirstIndexOf (x :: k) (xs :: [k]) :: Elem x xs where
FirstIndexOf x (x:xs) = Here
FirstIndexOf x (y:xs) = There (FirstIndexOf x xs)
-- INJect First
-- calculate the target index as a type
-- require it as an implicit value
-- defer to inj
injF :: forall as a.
KElem a as (FirstIndexOf a as) =>
a -> Sum as
injF = inj (demoteElem $ kElem @a @as @(FirstIndexOf a as))
-- or injF = inj (kElem :: SElem a as (FirstIndexOf a as))
Вы также можете просто вставить Elem внутрь Sum:
data Sum :: [*] -> * where
Sum :: !(Elem t ts) -> t -> Sum ts -- strictness optional
Вы можетевосстановить Inl и Inr как синонимы шаблона
pattern Inl :: forall ts. () =>
forall t ts'. (ts ~ (t : ts')) =>
t -> Sum ts
pattern Inl x = Sum Here x
data Inr' ts = forall t ts'. (ts ~ (t : ts')) => Inr' (Sum ts')
_Inr :: Sum ts -> Maybe (Inr' ts)
_Inr (Sum Here _) = Nothing
_Inr (Sum (There tag) x) = Just $ Inr' $ Sum tag x
pattern Inr :: forall ts. () =>
forall t ts'. (ts ~ (t : ts')) =>
Sum ts' -> Sum ts
pattern Inr x <- (_Inr -> Just (Inr' x))
where Inr (Sum tag x) = Sum (There tag) x
Если вы попробуете еще, вы можете использовать огромное количество unsafeCoerce Refl (для создания «поддельных» равенств типов), чтобы создать подобный API:
import Numeric.Natural
-- ...
type role SElem nominal nominal nominal
-- SElem is a GMP integer
-- Elem is a nice GADT
-- Elem gives a nice experience at the type level
-- this allows functions like FirstIndexOf
-- SElem avoids using unary numbers at the value level
newtype SElem x xs e = SElem Natural
pattern SHere :: forall t ts e. () =>
forall ts'. (ts ~ (t:ts'), e ~ (Here :: Elem t (t:ts'))) =>
SElem t ts e
pattern SThere :: forall t ts e. () =>
forall t' ts' e'. (ts ~ (t':ts'), e ~ (There e' :: Elem t (t':ts'))) =>
SElem t ts' e' ->
SElem t ts e
-- implementations are evil and kinda long
-- you'll probably need this:
-- type family Stuck (k :: Type) :: k where {- no equations -}
-- pattern synonyms are incredibly restrictive, so they aren't very straightforward
-- currently GHC does not allow INLINEs on pattern synonyms, so this won't
-- compile down to simple integer expressions just yet, either :(
И затем напишите
data Sum :: [*] -> * where
Sum :: forall t ts (e :: Elem t ts). !(SElem t ts e) -> t -> Sum ts
, что близко к struct целочисленного тега и union, за исключением того, что указанный тег немного увеличен.