1

我可以union在 Haskell 中有一个类型安全的联合（如 C 中的）吗？这是我尝试过的最好的，这里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.

我不明白这种歧义是如何出现的。

4

1 回答 1

4

构造函数的常规名称是Inland 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。这意味着您不能拥有仅具有“部分已知”变体的值。以下所有严格性注释都是为了“正确性”。他们在您可能不想要底部的地方挤压底部。

现在，singleton正如@rampion 所指出的，签名存在定义前使用错误。它“应该”是：

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

但这并不完全正确。如果a ~ b，太好了，这行得通。如果不是，则编译器无法确保它a在 in 中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 :: [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（创建“虚假”​​类型等式）来创建这样的 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整数标签的 a 和 a union，除了所述标签有点过大。

于 2018-05-27T03:16:04.197 回答