ECS Add Sum component

[paulcadman]

The Sum component allows cmap functions to set one of two alternatives.

The following function will delete the velocity component if the x component of the velocity is less than 5, otherwise will make no change.

f : Velocity -> Unit ⊕ Not Velocity
  | ⟨v⟩ => if v.x < 5
    then .inr .Not
    else .inl ()

[awalterschulze]

@paulcadman shouldn't it be returning the velocity it makes no changes to?

f : Velocity -> Velocity ⊕ Not Velocity
  | ⟨v⟩ => if v.x < 5
    then .inr .Not
    else .inl ⟨v⟩

[paulcadman]

@paulcadman shouldn't it be returning the velocity it makes no changes to?

f : Velocity -> Velocity ⊕ Not Velocity
  | ⟨v⟩ => if v.x < 5
    then .inr .Not
    else .inl ⟨v⟩

@awalterschulze both approaches work. My example uses the component instance and storage of Unit for which explSet is a no-op.

• ECS: Add Component instances for Unit #34

The advantage of using the Velocity -> Unit ⊕ Not Velocity approach here is that you can see from the type signature that either the Velocity component is deleted or the Velocity component is unchanged.

If you use Velocity -> Velocity ⊕ Not Velocity then the function may change the Velocity or delete the Velocity component.

I used this in the BouncingBall example in a function that either deletes a component or keeps everything the same as before.

raylean/lean/Examples/BouncingBall.lean

Lines 82 to 83 in 0210a8b

	/-- An alternative to `deleteAt` that uses a Sum to delete an entry --/
	def deleteAt'' (pos : Vector2) (radius : Float) : Position → System World (Unit ⊕ Not Position)

[awalterschulze]

Ok cool that makes sense, wow never would have thunk