是否可以有递归求和类型，每个“级别”都有不同的值？答案

【问题标题】：Is it possible to have recursive sum type, with each 'level' having distinct value?是否可以有递归求和类型，每个“级别”都有不同的值？
【发布时间】：2019-06-29 23:49:38
【问题描述】：

我想知道是否有可能（我猜是:)）有递归求和类型，其中我们在每个级别上都有一个 X 类型的值，但是以某种方式限制我们自己，在每个递归级别上，我们都有不同的值X？

例如，如果我有

data MachineType = Worker | Flyer | Digger | Observer | Attacker
data Machine = Single MachineType | Multi MachineType Machine

类型系统将允许我构建具有以下类型的机器：

Multi Worker (Multi Worker (Single Worker))

但我希望对此进行限制，以便只允许使用不同的 MachineType-s。

有没有办法在类型系统中对此进行编码？

你可以给我指出正确的方向，因为我有点不知道用谷歌搜索什么:)（haskell set-like recursive sum types？）

【问题讨论】：

您可以使用一个幻像类型参数，它是 MachineTypes 的类型级别 HList，并使 Machine 成为 GADT，其中构造函数需要证明该列表不包含给定类型的机器
@sara 的评论当然是一种方法，但使用Data.Set 并执行newtype Machine = Machine { getMachines :: Set MachineType } 不是更简单吗？
感谢您的回答！我将研究 HList 和 GADT 以了解它们是如何工作的。我也在考虑系列，但想知道这是否可以“高于”一级。我想编码的内容类似于 'X with added Y' 并且 set 可以解释为 'X with added Y' 和 'Y with添加 X'。使用模式匹配，我首先需要处理“主要”事物，即 X，然后如果我愿意，再向下递归到它的其他组件。但如果我不知道其他解决方案是如何工作的，它绝对是一个选择:)

标签： haskell

【解决方案1】：

一种解决方案是指定您不能使用重复的MachineType 扩展Machine。为此，我们首先需要为MachineType 提供singleton 类型：

{-# language TypeInType, GADTs, TypeOperators, ConstraintKinds,
    UndecidableInstances, TypeFamilies #-}

import Data.Kind
import GHC.TypeLits

data MachineType = Worker | Flyer | Digger | Observer | Attacker

data SMachineType t where
  SWorker   :: SMachineType Worker
  SFlyer    :: SMachineType Flyer
  SDigger   :: SMachineType Digger
  SObserver :: SMachineType Observer
  SAttacker :: SMachineType Attacker

然后我们指定一个约束，如果某些内容不包含在MachineTypes 列表中，则该约束是可满足的，否则抛出custom type error：

type family NotElem (x :: MachineType) (xs :: [MachineType]) :: Constraint where
  NotElem x '[]       = ()
  NotElem x (x ': xs) = TypeError
    (Text "Duplicate MachineTypes are not allowed in Machines" :$$:
    (Text "Can't add " :<>: ShowType x :<>: Text " to "
     :<>: ShowType (x ': xs)))
  NotElem x (y ': xs) = NotElem x xs

然后Machine 以 GADT 的形式给出，由 MachineTypes 的列表索引：

data Machine (ts :: [MachineType]) where
  Single :: SMachineType t -> Machine '[ t ]
  Multi  :: NotElem t ts => SMachineType t -> Machine ts -> Machine (t ': ts)

以下定义已推断出类型Machine '[ 'Flyer, 'Digger, 'Worker]：

m1 = Multi SFlyer (Multi SDigger (Single SWorker))

以下定义引发类型错误：

m2 = Multi SFlyer (Multi SFlyer (Single SWorker))

错误消息是：

   Notes.hs:30:6: error: …
    • Duplicate MachineTypes are not allowed in Machines
      Can't add 'Flyer to '[ 'Flyer, 'Worker]
    ...

【讨论】：

感谢一路上的示例和解释。得到它的工作，现在我将花一些时间来阅读你发布的关于 singleton 库的教程，以了解它“为什么”工作。干杯！

【解决方案2】：

看来我被打败了！作为对 András 回答的补充，我提出了一个类似的版本，但使用了每种机器类型唯一性的价值级别证明。

这在实际用例中可能不太符合人体工程学，但它确实具有某种“证明相关数学”的魅力（或者我自欺欺人地思考！）

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}

import Prelude

import Data.Kind (Type)
import Data.Void (Void)
import Data.Proxy (Proxy(..))

data MachineType
  = Worker
  | Flyer
  | Digger
  | Observer
  | Attacker
  deriving (Show, Eq)

data In xs x where
  Here :: forall k (xs :: [k]) (x :: k)
    . In (x ': xs) x
  There :: forall k (xs :: [k]) (x :: k) (y :: k)
    . In xs x -> In (y ': xs) x

type family Not a where
  Not a = (a -> Void)

data Machine :: [MachineType] -> Type where
  Single :: forall (t :: MachineType) (proxy :: MachineType -> Type)
    . proxy t -> Machine '[t]
  Multi :: forall (t :: MachineType) (ts :: [MachineType]) (proxy :: MachineType -> Type)
    . Not (In ts t) -> proxy t -> Machine ts -> Machine (t ': ts)

simpleMachine :: Machine '[ 'Worker ]
simpleMachine = Single Proxy

multiMachine :: Machine '[ 'Flyer, 'Attacker ]
multiMachine = Multi p (Proxy @'Flyer) $ Single (Proxy @'Attacker)
  where
    p :: Not (In '[ 'Attacker ] 'Flyer)
    p = \case
      There l -> case l of

【讨论】：