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.
我不明白这种歧义是怎么出现的。
构造函数的常规名称是 Inl 和 Inr:
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。此类型具有值 undefined、Left undefined 和 Right undefined，以及所有其他值。想想你的 Variant [a, b]。这有 undefined、Singleton undefined、Variant undefined 和 Variant (Singleton undefined)。 Either 不会出现一个额外的部分未定义值。 Inr 的严格性将 Inr undefined 和 undefined 压在一起。这意味着您不能拥有只有 "partially known" 变体的值。以下所有严格性注释均适用于 "correctness." 它们会在您可能不想要底部的地方压扁底部。
现在，正如@rampion 所指出的，singleton 的签名存在先用后定义错误。 "ought" 为：
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))
你也可以在 Sum 里面贴一个 Elem:
data Sum :: [Type] -> Type 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（创建 "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
接近整数标签的 struct 和 union，除了所述标签有点大。
我可以在 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.
我不明白这种歧义是怎么出现的。
构造函数的常规名称是 Inl 和 Inr:
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。此类型具有值 undefined、Left undefined 和 Right undefined，以及所有其他值。想想你的 Variant [a, b]。这有 undefined、Singleton undefined、Variant undefined 和 Variant (Singleton undefined)。 Either 不会出现一个额外的部分未定义值。 Inr 的严格性将 Inr undefined 和 undefined 压在一起。这意味着您不能拥有只有 "partially known" 变体的值。以下所有严格性注释均适用于 "correctness." 它们会在您可能不想要底部的地方压扁底部。
现在，正如@rampion 所指出的，singleton 的签名存在先用后定义错误。 "ought" 为：
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))
你也可以在 Sum 里面贴一个 Elem:
data Sum :: [Type] -> Type 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（创建 "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
接近整数标签的 struct 和 union，除了所述标签有点大。