Haskell 中的类型安全联合?

Type-safe union in Haskell?

我可以在 Haskell 中使用类型安全的联合(如 C 的 union)吗?这是我试过的最好的,这里 Variant,以 C++ 的 std::variant:

命名
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module Emulation.CPlusPlus.Variant (
    Variant, singleton
) where

import Data.Type.Bool
import Data.Type.Equality
import Type.Reflection

data Variant :: [*] -> * where
    Singleton :: a -> Variant (a ': as)
    Arbitrary :: Variant as -> Variant (a ': as)

singleton :: (Not (bs == '[]) || a == b) ~ 'True => forall a b. a -> Variant (b ': bs)
singleton x = case eqTypeRep (typeRep :: TypeRep a) (typeRep :: TypeRep b) of
    Nothing    -> Arbitrary (singleton x)
    Just HRefl -> Singleton x

这会产生如下错误消息:

Prelude> :load Variant.hs
[1 of 1] Compiling Emulation.CPlusPlus.Variant ( Variant.hs, interpreted )

Variant.hs:19:14: error:
    • Could not deduce: (Not (bs == '[]) || (a0 == b0)) ~ 'True
      from the context: (Not (bs == '[]) || (a == b)) ~ 'True
        bound by the type signature for:
                   singleton :: forall (bs :: [*]) a b.
                                ((Not (bs == '[]) || (a == b)) ~ 'True) =>
                                forall a1 b1. a1 -> Variant (b1 : bs)
        at Variant.hs:19:14-85
      The type variables ‘a0’, ‘b0’ are ambiguous
    • In the ambiguity check for ‘singleton’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        singleton :: (Not (bs == '[]) || a == b) ~ True =>
                     forall a b. a -> Variant (b : bs)
   |
19 | singleton :: (Not (bs == '[]) || a == b) ~ True => forall a b. a -> Variant (b ': bs)
   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

我不明白这种歧义是怎么出现的。

构造函数的常规名称是 InlInr:

import Data.Kind

data Sum :: [Type] -> Type where
  Inl :: a -> Sum (a : as) -- INject Left
  Inr :: !(Sum as) -> Sum (a : as) -- INject Right

Inr 中的额外严格性是可选的。考虑 Either a b。此类型具有值 undefinedLeft undefinedRight undefined,以及所有其他值。想想你的 Variant [a, b]。这有 undefinedSingleton undefinedVariant undefinedVariant (Singleton undefined)Either 不会出现一个额外的部分未定义值。 Inr 的严格性将 Inr undefinedundefined 压在一起。这意味着您不能拥有只有 "partially known" 变体的值。以下所有严格性注释均适用于 "correctness." 它们会在您可能不想要底部的地方压扁底部。

现在,正如@rampion 所指出的,singleton 的签名存在先用后定义错误。 "ought" 为:

singleton :: forall a b.
             (Not (bs == '[]) || a == b) ~ True =>
             a -> Variant (b ': bs)

但这并不完全正确。如果 a ~ b,太好了,这行得通。如果不是,编译器就无法确保 abs 中,因为您没有对此进行约束。这个新签名仍然失败。对于最强大的功能,尤其是对于未来的定义,您需要像

这样的东西
-- 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))

你也可以在 Sum 里面贴一个 Elem:

data Sum :: [Type] -> Type where
  Sum :: !(Elem t ts) -> t -> Sum ts -- strictness optional

您可以恢复 InlInr 作为模式同义词

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(创建 "bogus" 类型等式)来创建这样的 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 :: [Type] -> Type where
  Sum :: forall t ts (e :: Elem t ts). !(SElem t ts e) -> t -> Sum ts

接近整数标签的 structunion,除了所述标签有点大。