<div dir="ltr">You'd need GHC extensions to pull that off, Greg, but it could be done. Something like<div><br></div><div>data Vect (size :: Nat) (a :: *) where</div><div> Cons :: a -> Vect n a -> Vect (Succ n) a</div>
<div> Nil :: Vect Zero a</div><div><br></div><div>data NatUpTo (n :: Nat) where</div><div> Here :: NatUpTo n -- "Here" means 0</div><div> There :: NatUpTo n -> NatUpTo (S n) -- "There x" means 1 + x</div>
<div><br></div><div>vectIndex :: Vect (S n) a -> NatUpTo n -> a<br></div><div>vectIndex (Cons x _) Here = a</div><div>vectIndex (Cons _ xs) (There i) = vectIndex xs i</div><div><br></div><div>class (Enum a) => EnumSize (size :: Nat) a where</div>
<div> enumerateAll :: Vect size a</div><div> -- law: (enumerateAll `asTypeOf` [x]) `vectIndex` unsafeIntToNatUpTo (fromEnum x)</div><div><br></div><div>It gets tedious, though, dealing with all of that safety. LiquidHaskell is perhaps a more viable option for such a thing. It would be nice to have standard libraries written with LiquidHaskell so that we have a more rigorously proven code base.</div>
</div><div class="gmail_extra"><br clear="all"><div>-- Dan Burton</div>
<br><br><div class="gmail_quote">On Wed, Sep 11, 2013 at 10:57 AM, Greg Fitzgerald <span dir="ltr"><<a href="mailto:garious@gmail.com" target="_blank">garious@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I'd prefer something more like:<br>
<br>
mux :: Enum b => [a] -> b -> a<br>
mux xs x = xs !! fromEnum x<br>
<br>
so then 'bool' could be implemented as:<br>
<div class="im"><br>
bool :: a -> a -> Bool -> a<br>
</div> bool f t = mux [f, t]<br>
<br>
but 'mux' needs a stronger type signature. The size of the enum is<br>
known at compile-time. Is there any way to constrain the input list<br>
to be the same size?<br>
<br>
Thanks,<br>
Greg<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
On Wed, Sep 11, 2013 at 2:18 AM, Simon Hengel <<a href="mailto:sol@typeful.net">sol@typeful.net</a>> wrote:<br>
> On Tue, Sep 10, 2013 at 11:02:19PM +0100, Oliver Charles wrote:<br>
>> I would like to propose that the following is added to Data.Bool in base:<br>
>><br>
>> bool :: a -> a -> Bool -> a<br>
>> bool f _ False = f<br>
>> bool _ t True = t<br>
><br>
> +1<br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
> <a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/libraries" target="_blank">http://www.haskell.org/mailman/listinfo/libraries</a><br>
</div></div></blockquote></div><br></div>