The start of a small implementation of well-typed ECS in Idris

ECS.idr

||| A well-typed entity component system
||| The goal of an entity component system is to be able to deal with a heterogenous
||| collection of objects some of which share a set of features or interfaces.
module ECS

import Data.List
import Data.Maybe
import Data.Product
import Data.List.Quantifiers

-- We need to remove those in order to use parenthesis in our DSL
%hide Builtin.Pair
%hide Builtin.MkPair

-- This is the operator for building recod fields
infixr 5 :-:

-- First we define a small type universe with the types we expect to use
-- Nothing fancy, just base types and no recursion nor variables
data Universe
  = (:-:) String Universe
  | Both Universe Universe
  | Choice Universe Universe
  | UInt
  | UString
  | UDouble
  | UNat
  | UVoid

-- We use this trick to use parenthesis for defining records
namespace Builtin
  public export
  Pair : Universe -> Universe -> Universe
  Pair = Both


-- We interpret our universe as an idris type to build some inhabitants
Interpret : Universe -> Type
Interpret (str :-: x) = Interpret x -- for fields we throw away the tag
Interpret (Both x y) = Interpret x * Interpret y
Interpret (Choice x y) = Either (Interpret x) (Interpret y)
Interpret UInt = Int
Interpret UString = String
Interpret UDouble = Double
Interpret UNat = Nat
Interpret UVoid = Unit

-- Sometimes we need to know if a piece of data contains a certain field
-- This data structure carries evidence that a piece of data contains a field with the given type
data HasField : (f : String) -> (ty, u : Universe) -> Type where
  This : HasField fname ty (fname :-: ty)
  InLeft : HasField f ty a -> HasField f ty (Both a b)
  InRight : HasField f ty b -> HasField f ty (Both a b)

-- We define Booleans in our universe as a coproduct of two fields
TBool : Universe
TBool = Choice ("true" :-: UVoid) ("false" :-: UVoid)

false : Interpret TBool
false = Left ()

true : Interpret TBool
true = Right ()

-- We define a knife object which is both a weapon and a kitchen item
TKnife : Universe
TKnife = ( "name" :-: UString
         , "speed" :-: UInt
         , "power" :-: UInt
         , "kitchen" :-: UVoid
         , "weapon" :-: UVoid
         )

-- We define a spoon which is just a kitchen item
TSpoon : Universe
TSpoon = ( "name" :-: UString
         , "kitchen" :-: UVoid
         )

-- We define a sword that is only a weapon and nothing else
TSword : Universe
TSword = ( "name" :-: UString
         , "weapon" :-: UVoid
         , "power" :-: UInt
         , "speed" :-: UInt
         , "isDamaged" :-: TBool
         )

-- We collect all our items in a heterogenous list
items : All Interpret [TKnife, TSpoon, TSword]
items = [baseKnife, baseSpoon, baseSword]
  where
    baseKnife : Interpret TKnife
    baseKnife = "Victorniox" && 5 && 10 && () && ()
    baseSpoon : Interpret TSpoon
    baseSpoon = "Grandma's spoon" && ()
    baseSword : Interpret TSword
    baseSword = "One Hand Sword" && ()  && 35 && 10 && false

-- We can also hide the list of types from the typesystem and have it be carried by the runtime
record OpaqueContainer where
  constructor MkOpaque
  types : List Universe
  content : All Interpret types

-- We can now carry our list of items in an opaque container:
opaqueItems : OpaqueContainer
opaqueItems = MkOpaque [TKnife, TSpoon, TSword] items

-- We can add items to our list of opaque things
cons : (ty : Universe ** Interpret ty) -> OpaqueContainer -> OpaqueContainer
cons (ty ** val) container = MkOpaque (ty :: container.types) (val :: container.content)

-- Now let's add another knife to the list
moreItems : OpaqueContainer
moreItems = cons (TKnife ** cheesyKnife) opaqueItems
  where
    cheesyKnife : Interpret TKnife
    cheesyKnife = "Cheese Knife" && 12 && 2 && () && ()

-- we can write a function that extract a weapon
isWeapon : (t : Universe) ->  Maybe (HasField "weapon" UVoid t)
isWeapon ("weapon" :-: UVoid) = Just This
isWeapon (Both y z) = map InLeft (isWeapon y) <|> map InRight (isWeapon z)
isWeapon _ = Nothing

-- The next two functions are utilities, one to map from a heterogenous list to a
-- list of existentials pairs
asPairs : {tys : _} -> All Interpret tys -> List (x : Universe ** Interpret x)
asPairs [] = []
asPairs {tys = t :: ts} (x :: xs) = (t ** x) :: asPairs xs

-- The second to map froma list of existential pairs to a heterogenous list
fromPairs : (tys : List (x : Universe ** Interpret x)) -> All Interpret (map fst tys)
fromPairs [] = []
fromPairs ((t ** val) :: xs) = ?shouldBeVal :: fromPairs xs

-- now we can write a function to filter all the weapons
-- We can write a function that will return all weapons from a list of items
allWeapons : OpaqueContainer -> (List (x : Universe ** Interpret x))
allWeapons (MkOpaque tys con) =
  let types : List (x : Universe ** Interpret x)
      types = asPairs con
      weapons : List (Bool * (x : Universe ** Interpret x))
      weapons = map (\(ty ** val) => isJust (isWeapon ty) && (ty ** val)) types
  in map snd $ filter fst weapons
  
-- Todo: 
-- - generalise the previous function for any field
-- - refactor any "weapon" and "kitchen" types as their own tagged types
-- - perform state updates with an opake list of items in the state. possibly using lenses