haskell - 是否可以有递归求和类型，每个 'level' 都有不同的值？

Question

我想知道是否有可能(我猜是:))有递归求和类型，其中我们在每个级别上都有一个 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？)

Answer 1

一种解决方案是指定您不能扩展 Machine带有重复的 MachineType .为此，我们首先需要一个 singleton输入 MachineType :

{-# 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

然后我们指定一个可以满足的约束，如果某些内容不包含在 MachineType 的列表中。 s，否则抛出 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以 MachineType 列表索引的 GADT 形式给出年代:

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]
    ...