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

user_7292889 0
Viewed 319

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?)

haskell
2 Answers

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

It seems I was beaten to it! As a complement to András' answer, I came up with a version that is similar, but uses value level proofs of the uniqueness of each machine type.

This is probably less ergonomic in practical use cases, but it does have a certain "proof relevant mathematics" charm (or so I delude myself into thinking!)

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