<div dir="ltr">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. <br><div><br></div><div>I vaguely recall using a GADT+typeclass strategy something like this to check this at compile time:</div><div><br></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">data Stage = F</span><span style="color:rgb(36,41,47);font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre"> | </span><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">D</span><span style="color:rgb(36,41,47);font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre"> | </span><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">R</span><span style="color:rgb(36,41,47);font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre"> | </span><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">X -- fetch/decode/read/execute</span><br></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">data Instruction allowed where</span></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">    MemRead :: MemAddress -> Register -> Instruction [F,D,R]</span></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">    RegWrite :: Word64 -> Register -> Instruction [F,D,R,X]</span></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">    ...</span></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre"><br></span></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">-- Type-level list membership</span></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">executeR :: (Contains R in, Contains X out) => ReadContext -> Instruction in -> (ReadResult, Instruction out)</span></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">executeR ctx (MemRead a r) = ...</span></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre">executeR ctx (RegWrite w r) = ...</span></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre"><br></span></div><div><font face="ui-monospace, SFMono-Regular, SF Mono, Menlo, Consolas, Liberation Mono, monospace"><span style="font-size:12px;white-space:pre">executeX :: Contains X in => ExecutionContext -> Instruction in -> ExecutionResult</span></font></div><div><font face="ui-monospace, SFMono-Regular, SF Mono, Menlo, Consolas, Liberation Mono, monospace"><span style="font-size:12px;white-space:pre">executeX ctx (RegWrite w r) = ...</span></font></div><div><font face="ui-monospace, SFMono-Regular, SF Mono, Menlo, Consolas, Liberation Mono, monospace"><span style="font-size:12px;white-space:pre"><br></span></font></div><div><span style="font-size:12px;white-space:pre"><font face="arial, sans-serif">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,</font></span></div><div><span style="font-size:12px;white-space:pre"><font face="arial, sans-serif">and would not give me spurious exhaustiveness warnings.</font></span></div><div><br></div><div><font face="arial, sans-serif"><span style="font-size:12px;white-space:pre">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.</span></font></div><div><font face="arial, sans-serif"><span style="font-size:12px;white-space:pre"><br></span></font></div><div><font face="arial, sans-serif"><span style="font-size:12px;white-space:pre">Will</span></font></div><div><span class="gmail-pl-ent" style="box-sizing:border-box;font-family:ui-monospace,SFMono-Regular,"SF Mono",Menlo,Consolas,"Liberation Mono",monospace;font-size:12px;white-space:pre"><br></span></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Aug 30, 2022 at 11:09 AM David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="auto">One downside of this *particular* formulation is that it doesn't play well with Coercible.</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Aug 30, 2022, 9:31 AM Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de" target="_blank">olf@aatal-apotheke.de</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">Dear Café,<br>
<br>
Is there prior art/existing packages for the following? Is it maybefunctional programming folklore? Is it a sign of bad program design? <br>
Sometimes I feel the need to selectively allow or disallow alternatives<br>
in a sum type. That is, suppose we have a sum type<br>
<br>
data Foo = LeftFoo !A | RightFoo !B<br>
<br>
and at some places in the program we want the type system to enforce<br>
that only the constructor LeftFoo can be used. My solution would be to<br>
use a strict version of Data.Functor.Const and make the type higher<br>
rank:<br>
<br>
newtype Const' a b = Const' !a<br>
-- Const' Void b ~ Void<br>
-- Const' ()   b ~ ()<br>
<br>
data Foo' f = LeftFoo' !A | RightFoo' !(f B)<br>
type Foo = Foo' Identity<br>
type LeftFoo = Foo' (Const' Void) -- can not construct a RightFoo'<br>
<br>
The advantage over defining LeftFoo as an entirely different type is<br>
that Foo and LeftFoo can share functions operating entirely on the left<br>
option. <br>
<br>
Olaf<br>
<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>