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 On Tue, Aug 30, 2022 at 11:09 AM David Feuer <david.feuer@gmail.com> wrote:
One downside of this *particular* formulation is that it doesn't play well with Coercible.
On Tue, Aug 30, 2022, 9:31 AM Olaf Klinke <olf@aatal-apotheke.de> wrote:
Dear Café,
Is there prior art/existing packages for the following? Is it maybefunctional programming folklore? Is it a sign of bad program design? Sometimes I feel the need to selectively allow or disallow alternatives in a sum type. That is, suppose we have a sum type
data Foo = LeftFoo !A | RightFoo !B
and at some places in the program we want the type system to enforce that only the constructor LeftFoo can be used. My solution would be to use a strict version of Data.Functor.Const and make the type higher rank:
newtype Const' a b = Const' !a -- Const' Void b ~ Void -- Const' () b ~ ()
data Foo' f = LeftFoo' !A | RightFoo' !(f B) type Foo = Foo' Identity type LeftFoo = Foo' (Const' Void) -- can not construct a RightFoo'
The advantage over defining LeftFoo as an entirely different type is that Foo and LeftFoo can share functions operating entirely on the left option.
Olaf
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.