Proposal: Add bool to Data.Bool

[Dan Burton]

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 at 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 at 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 at haskell.org
> > http://www.haskell.org/mailman/listinfo/libraries
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130911/6fdd47d9/attachment.htm>