[Haskell-cafe] selectively allow alternatives in a sum type

[William Yager]

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 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
>> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220830/7f66c8d3/attachment.html>