总集合,拒绝不包括所有可能性的类型集合

Question

假设我们有以下类型:

sealed trait T
case object Goat extends T
case object Monk extends T
case object Tiger extends T

现在,如何构建一个集合,T使得每个子集中至少有一个T出现在集合中,这个约束是在编译时强制执行的？一个集合,与此相反:

val s:Seq[T] = Seq(Goat)

编译,这:

val ts:TotalSeq[T] = TotalSeq(Goat, Goat, Tiger)

才不是.我上面使用过Scala,但我很乐意看到其他语言的解决方案.

(请原谅我,如果我的话有点偏;我感冒了,今天我很开心,有谜题.)

Answer 1

它看起来像具有通用类型约束的构建器模式:http://www.tikalk.com/java/blog/type-safe-builder-scala-using-type-constraints

就像是:

sealed trait TBoolean
sealed trait TTrue extends TBoolean
sealed trait TFalse extends TBoolean

class SeqBuilder[HasGoat <: TBoolean, HasMonk <: TBoolean, HasTiger <: TBoolean] private (seq: Seq[T]) {

  def +=(g: Goat.type) = new SeqBuilder[TTrue, HasMonk, HasTiger](g +: seq)

  def +=(m: Monk.type) = new SeqBuilder[HasGoat, TTrue, HasTiger](m +: seq)

  def +=(t: Tiger.type) = new SeqBuilder[HasGoat, HasMonk, TTrue](t +: seq)

  def build()(implicit evg: HasGoat =:= TTrue, evm: HasMonk =:= TTrue, evt: HasTiger =:= TTrue) = seq
}


object SeqBuilder {
  def apply = new SeqBuilder(Seq())
}

用法:

scala> SeqBuilder() + Goat + Tiger + Monk build()
res21: Seq[T] = List(Monk, Tiger, Goat)

scala> SeqBuilder() + Goat + Goat + Monk build()
<console>:34: error: Cannot prove that Nothing =:= TTrue.
       SeqBuilder() + Goat + Goat + Monk build()
                                         ^

如果您想要的实例数增加,您可以尝试使用HMap

其他类似方法:幻像类型:http://james-iry.blogspot.com/2010/10/phantom-types-in-haskell-and-scala.html

另一种方法是询问为什么需要所有3个对象.假设您想要在seq全部三个时进行操作,那么您可以执行以下操作:

object SeqBuilder {
  val all = Seq(Goat, Monk, Tiger)

  def apply(t: T*)(onAll: Seq[T] => Unit)(onViolation: => Unit) = {
     val seq = Seq(t:_*)
     if(all forall seq.contains) onAll(seq)
     else onViolation
  }
}

这样,如果没有提供所有必需的Ts,则不调用onAll函数,否则调用违规函数

Answer 2

如果我正确地解释这个......

{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}

data Goat
data Monk
data Tiger

data T a where
    TGoat  :: T Goat
    TMonk  :: T Monk
    TTiger :: T Tiger

data TSeq a where
    TNil :: TSeq ((), (), ())
    TG   :: T Goat -> TSeq ((), m, t) -> TSeq (Goat, m, t)
    TM   :: T Monk -> TSeq (g, (), t) -> TSeq (g, Monk, t)
    TT   :: T Tiger -> TSeq (g, m, ()) -> TSeq (g, m, Tiger)
    TCG  :: T Goat -> TSeq (Goat, m, t) -> TSeq (Goat, m, t)
    TCM  :: T Monk -> TSeq (g, Monk, t) -> TSeq (g, Monk, t)
    TCT  :: T Tiger -> TSeq (g, m, Tiger) -> TSeq (g, m, Tiger)

请注意,没有尝试使其可用.这非常笨拙.

现在,给出这些值:

x = TCG TGoat (TG TGoat (TT TTiger (TM TMonk TNil)))

y = TG TGoat TNil

而这个功能:

f :: TSeq (Goat, Monk, Tiger) -> a
f _ = undefined

...然后只会f x打字检查,而不是f y.

NB从序列中删除项目留给读者练习.

编辑:经过进一步的考虑,我已经认定上述情况并不是很糟糕.看吧:

一些神秘熟悉的样板:

data Yes = Yes
data No = No

class TypeEq' () x y b => TypeEq x y b | x y -> b
instance TypeEq' () x y b => TypeEq x y b

class TypeEq' q x y b | q x y -> b
class TypeEq'' q x y b | q x y -> b


instance TypeCast b Yes => TypeEq' () x x b
instance TypeEq'' q x y b => TypeEq' q x y b
instance TypeEq'' () x y No

class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x  = x

一般的hackery:

infixr 1 :*:
data NIL
data h :*: t = h :*: t

class TIns x ys r | x ys -> r
instance TIns x NIL (x :*: NIL)
instance ( TypeEq x h b 
         , TIns' b x h t r
         ) => TIns x (h :*: t) r


class TIns' b x h t r | b x h t -> r
instance TIns' Yes x h t (h :*: r)
instance (TIns x t r) => TIns' No x h t (h :*: r)


class TElem x ys r | x ys -> r
instance TElem x NIL No
instance (TypeEq x h b, TElem' b x h t r) => TElem x (h :*: t) r

class TElem' b x h t r | b x h t -> r
instance TElem' Yes x h t Yes
instance (TElem x t r) => TElem' No x h t r

Aaaaaaa和收益:

data TSeq2 a b where
    TNil2  :: TSeq2 NIL NIL
    TCons2 :: (TIns x ys r) => T x -> TSeq2 xs ys -> TSeq2 (x :*: xs) r

class (TElem x ys Yes) => Has ys x
instance (TElem x ys Yes) => Has ys x

class HasAll ys xs
instance HasAll ys NIL
instance (ys `Has` h, ys `HasAll` t) => HasAll ys (h :*: t)

x2 = TCons2 TGoat (TCons2 TGoat (TCons2 TTiger (TCons2 TMonk TNil2)))

y2 = TCons2 TGoat TNil2

f2 :: (s `HasAll` (Goat :*: Tiger :*: Monk :*: NIL)) => TSeq2 q s -> a
f2 _ = undefined

与上面一样,f2 x2typechecks虽然f2 y2失败了.

这仍然是凌乱的,使用起来相当痛苦,但更通用!

并且为了证明在其他情况下结果仍然可以被视为普通数据类型,这里有一个实例Show:

instance Show (T a) where
    show TGoat = "TGoat"
    show TMonk = "TMonk"
    show TTiger = "TTiger"

instance Show (TSeq2 a b) where
    show TNil2 = "[]"
    show (TCons2 x xs) = concat [show x, ":", show xs]

所以现在我们可以做show只包含所有三种项目的序列:

showTotal :: (s `HasAll` (Goat :*: Tiger :*: Monk :*: NIL)) => TSeq2 q s -> String
showTotal = show