In university, I wrote a bunch of CPUs in clash/haskell for an FPGA CPU design class. In one pipelined scalar CPU, I had a number of CPU instructions, and as the instructions moved down the pipe, the set of allowed instructions would change. E.g. a memory read instruction would eventually get changed to a register write instruction, and there was no reason to permit a memory read instruction to be representable after the memory read stage of the pipeline.
I vaguely recall using a GADT+typeclass strategy something like this to check this at compile time:
data Stage = F | D | R | X -- fetch/decode/read/execute
data Instruction allowed where
MemRead :: MemAddress -> Register -> Instruction [F,D,R]
RegWrite :: Word64 -> Register -> Instruction [F,D,R,X]
...
-- Type-level list membership
executeR :: (Contains R in, Contains X out) => ReadContext -> Instruction in -> (ReadResult, Instruction out)
executeR ctx (MemRead a r) = ...
executeR ctx (RegWrite w r) = ...
executeX :: Contains X in => ExecutionContext -> Instruction in -> ExecutionResult
executeX ctx (RegWrite w r) = ...
If I'm remembering this correctly, Haskell's `GADTs meet their match` based type checker was smart enough to know when a constructor was not allowed for a function,
and would not give me spurious exhaustiveness warnings.
I think I had another strategy still using typeclasses, but not using type-level lists/sets, but I can't remember what it would have been.
Will