是否可以具有递归和类型，而每个“级别”具有不同的值？

Question

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

例如，如果我有

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

类型系统将允许我构造以下类型的Machine：

Multi Worker (Multi Worker (Single Worker))

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

有没有一种方法可以在类型系统中对此进行编码？

您可以为我指明正确的方向，因为我有点不知道该对Google进行什么操作：）（类似于haskell集的递归和类型？）

Answer 1

一种解决方案是指定您不能Machine使用重复项来扩展MachineType。为此，我们首先需要一个单例类型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

然后，我们指定一个约束，如果MachineTypes 列表中未包含某些内容，则可以满足该约束，否则将引发自定义类型错误：

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给出为由MachineTypes 列表索引的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]
    ...