[Haskell-cafe] selectively allow alternatives in a sum type
will.yager at gmail.com
Tue Aug 30 20:53:08 UTC 2022
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 ->
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.
On Tue, Aug 30, 2022 at 11:09 AM David Feuer <david.feuer at 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 at 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
>> 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
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> 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:
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe