You'd need GHC extensions to pull that off, Greg, but it could be done. Something like data Vect (size :: Nat) (a :: *) where Cons :: a -> Vect n a -> Vect (Succ n) a Nil :: Vect Zero a data NatUpTo (n :: Nat) where Here :: NatUpTo n -- "Here" means 0 There :: NatUpTo n -> NatUpTo (S n) -- "There x" means 1 + x vectIndex :: Vect (S n) a -> NatUpTo n -> a vectIndex (Cons x _) Here = a vectIndex (Cons _ xs) (There i) = vectIndex xs i class (Enum a) => EnumSize (size :: Nat) a where enumerateAll :: Vect size a -- law: (enumerateAll `asTypeOf` [x]) `vectIndex` unsafeIntToNatUpTo (fromEnum x) 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. -- Dan Burton On Wed, Sep 11, 2013 at 10:57 AM, Greg Fitzgerald <garious@gmail.com> wrote:
I'd prefer something more like:
mux :: Enum b => [a] -> b -> a mux xs x = xs !! fromEnum x
so then 'bool' could be implemented as:
bool :: a -> a -> Bool -> a bool f t = mux [f, t]
but 'mux' needs a stronger type signature. The size of the enum is known at compile-time. Is there any way to constrain the input list to be the same size?
Thanks, Greg
On Wed, Sep 11, 2013 at 2:18 AM, Simon Hengel <sol@typeful.net> wrote:
On Tue, Sep 10, 2013 at 11:02:19PM +0100, Oliver Charles wrote:
I would like to propose that the following is added to Data.Bool in base:
bool :: a -> a -> Bool -> a bool f _ False = f bool _ t True = t
+1 _______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries
Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries