Re: Proposal: Add bool to Data.Bool

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 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 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

On Wed, Sep 11, 2013 at 2:18 AM, Simon Hengel wrote: 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