I am modeling a system that has an operation that creates a resource and other operations that consume that resource. However, a given resource can only be consumed once - is there a way that I can guarantee that at compile time?
For concreteness, lets say the first operation bakes a cake and that there are two other operations, one for "choosing to eat" the cake and one for "choosing to have the cake" and that I can only do one or the other.
-- This is my current "weakly typed" interface:
bake :: IO Cake
eat :: Cake -> IO ()
keep :: Cake -> IO ()
-- This is OK
do
brownie <- bake
muffin <- bake
eat brownie
keep muffin
-- Eating and having the same cake is not OK:
do
brownie <- bake
eat brownie
keep brownie -- oops! already eaten!
Its easy to enforce the restriction of not keeping an already eaten cake (or vice versa) at runtime by setting an flag on the cake after we use it. But is there a way to enforce this at compile time?
BTW, this question is meant for a proof of concept so I am OK with any black magic that can give me the static safety I want.
In Haskell, a basic version of this could be expressed with a GADT indexed by a store of cakes (represented by a list of
Nat
-s):Unfortunately we can't remove the type annotations from
Bake
actions and leave types to be inferred:Obviously,
(Elem (New cs0) (New cs0 + 1 : New cs0 : cs0))
is satisfiable for allcs0
, but GHC can't see this, because it cannot decide whetherNew cs0
is inequal toNew cs0 + 1
, because GHC can't assume anything about the flexiblecs0
variable.If we add
NoMonomorphismRestriction
,foo
would typecheck, but that would make even incorrect programs typecheck by pushing all theElem
constraints to the top. This would still prevent doing anything useful with incorrect terms though, but it's a rather ugly solution.More generally, we can express
Bake
as an indexed free monad, which gets usdo
-notation withRebindableSyntax
, and allows a definition forBakeF
that is somewhat clearer than what we've seen before. It could also reduce boilerplate much like the plain oldFree
monad, although I find it rather unlikely that people would find use for indexed free monads on two different occasions in practical code.