Is it possible to have recursive sum type, with each 'level' having distinct value?

Question

I was wondering if it is possible (I guess it is :) ) to have recursive sum type where we have a value of type X on every level, but somehow restrict ourselves that on every level of recursion we have distinct value of X?

For example, if I have

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

type system would allow me to construct Machine with following type:

Multi Worker (Multi Worker (Single Worker))

but I want this to be restricted, so that only different MachineType-s are allowed.

Is there a way to encode this in type system?

You can just point me in the right direction, as I kinda don't know what to google :) (haskell set-like recursive sum types?)

Answer 1

One solution is to specify that you can't extend a Machine with a duplicate MachineType. For that we first need a singleton type for 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

Then we specify a constraint which is satisfiable if something is not contained in a list of MachineTypes, and otherwise throws a 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

Then Machine is given as a GADT indexed by lists of MachineTypes:

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

The following definition has inferred type Machine '[ 'Flyer, 'Digger, 'Worker]:

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

The following definition throws a type error:

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

With the error message being:

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