- Libraries - Haskell.org

Pattern synonyms and record fields for Cont, Writer, Reader, State, ...
by Baldur Blöndal 22 Nov '16

22 Nov '16

This will look like the original definitions [1] > newtype State s a = State { runState :: s -> (a, s) } before they became type synonyms > type State s = StateT s Identity by defining pattern synonyms > pattern State :: (s -> (a, s)) -> State s a > pattern State {runState} <- S.runState -> runState > where State a = state a Trac ticket #12767 for further information. [2] [1] http://book.realworldhaskell.org/read/monads.html#id643643 [2] https://ghc.haskell.org/trac/ghc/ticket/12767

2 2

Add ifThenElse and (?) to Data.Bool
by winter 21 Nov '16

21 Nov '16

It seems this’s a very old request, see https://wiki.haskell.org/If-then-else <https://wiki.haskell.org/If-then-else>. I’d like to see following: ifThenElse :: Bool -> a -> a -> a ifThenElse True x _ = x ifThenElse False _ y = y infixr 1 ? (?) :: Bool -> a -> a -> a (?) = ifThenElse in Date.Bool module, it will have advantages that: + It’s more composable than syntax. + Write (xxx ? yyy $ zzz) instead of (if xxx then yyy else zzz) is more consistent with (f . g $ x) style, and save key strokes. + In module with RebindableSyntax enabled, you can import ifThenElse to get default behavior. Whether or not to be exported by Prelude is another question, but Data.Bool seems a good place to start with. Cheers~ Winter

9 16

Add default MonadPlus or Alternative method to MonadFail
by Baldur Blöndal 17 Nov '16

17 Nov '16

The documentation for Control.Monad.Fail notes > If your Monad is also MonadPlus, a popular definition is >> fail _ = mzero This could be made a default definition for MonadPlus or Alternative > class Monad m => MonadFail m where > fail :: String -> m a > fail = const empty > default fail :: Alternative m => String -> m a This simplifies instances like [] and Maybe > instance MonadFail [] > instance MonadFail Maybe

1 0

Re: Proposal: Add portable eliminator for Data.Type.Equality
by David Feuer 15 Nov '16

15 Nov '16

On Nov 15, 2016 12:24 AM, "wren romano" <winterkoninkje(a)gmail.com> wrote: > > subst :: a :~: b -> f a -> f b > > subst Refl x = x > > I'm all for adding this function, but do note that the type is > suboptimal since GHC lacks general functions (and higher-order pattern > matching) at the type level. Which means we'll actually end up wanting > a family of different "subst" functions to cover all the (relevant) > cases the definition above would cover in a language like Agda, Coq, > etc. Yes, we will, but those can be written using `subst` and one or more auxiliary types without additional "primitive" eliminators (see below). > E.g., > > Prelude> let x :: Either Bool Int; x = Right 42 > > Prelude> :t (`subst` x) > (`subst` x) :: Int :~: b -> Either Bool b > > When I might've really wanted/meant (Bool :~: b -> Either b Int) We can write newtype Flip f x y = Flip { unFlip :: f y x } subst2 :: a :~: b -> f a x -> f b x subst2 eq = unFlip . subst eq . Flip The subst2 function will work on the left side of Either.

2 2

Proposal: Add ‘type f ~> g = forall a. f a -> g a’
by Baldur Blöndal 15 Nov '16

15 Nov '16

What the subject says, add type f ~> g = forall a. f a -> g a to ‘base’. Further motivation (and arguments against) in GHC Trac ticket 12772 [1]. [1] https://ghc.haskell.org/trac/ghc/ticket/12772

6 5

Proposal: Add portable eliminator for Data.Type.Equality
by David Feuer 15 Nov '16

15 Nov '16

Most of Data.Type.Equality can be supported by any Haskell implementation with Rank2Types and TypeOperators, using, for example, the well-known definition newtype a :~: b = Equality { subst :: forall f . f a -> f b } (The parts that can't be supported so are the gcastWith function, the ~~ constraint, and the == type family.) What's most prominently missing is the ability to *use* equality for anything beyond castWith without leaning on GHC's equality constraints. I propose that we add the eliminator subst as a function: subst :: a :~: b -> f a -> f b subst Refl x = x Note that we already have an introduction rule Control.Category.id :: a :~: a David Feuer

2 2

Proposal: relax type of asProxyTypeOf
by Tom Ellis 09 Nov '16

09 Nov '16

Did anything ever come of this proposal to relax the type of asProxyType of? https://mail.haskell.org/pipermail/libraries/2014-December/024462.html i.e. change asProxyTypeOf :: a -> Proxy a -> a to asProxyTypeOf :: a -> proxy a -> a I posted this issue on the Trac https://ghc.haskell.org/trac/ghc/ticket/12805 but it was suggested I ask on the libraries list. Tom

4 3

Re: Proposal: relax type of asProxyTypeOf
by Ryan Scott 07 Nov '16

07 Nov '16

Oh, I didn't realize that the type had already been generalized in tagged! [1] I'm certainly +1 on this proposal. Ryan S. ----- [1] https://github.com/ekmett/tagged/blob/93cd87830733ed641409a2a14776973e8be60…

1 0

Type Level "Application" Operator
by Elliot Cameron 03 Nov '16

03 Nov '16

Folks, Has there been a discussion about adding a type-level operator "$" that just mimics "$" at the value level? type f $ x = f x infixr 0 $ Things like monad transformer stacks would look more "stack-like" with this: type App = ExceptT Err $ ReaderT Config $ LogT Text IO Elliot Cameron

7 10

Discussion: add pattern synonyms and a non-dependent eliminator to Numeric.Natural
by David Feuer 03 Nov '16

03 Nov '16

Pattern synonyms: pattern Successor :: Natural -> Natural pattern Successor n <- (precMaybe -> Just n) where Successor n = n + 1 precMaybe :: Natural -> Maybe Natural precMaybe 0 = Nothing precMaybe n = Just (n - 1) pattern Zero :: Natural pattern Zero = 0 Eliminator: toChurch :: Natural -> (a -> a) -> a -> a toChurch 0 _ b = b toChurch n f b = f (toChurch (n-1) f b) There are several other possible argument orders, the most natural of which is probably natural :: a -> (a -> a) -> Natural I don't have particularly strong feelings about whether we should pick one or offer both. There are two strictly accumulating versions, corresponding to different versions of foldl'. But toChurch/natural is sufficient to define them: toChurch', toChurch'' :: Natural -> (a -> a) -> a -> a toChurch' n f = toChurch n (\r acc -> r $! f acc) id toChurch'' n f = toChurch n (\r !acc -> r $ f acc) id So we shouldn't necessarily feel obligated to include those. I doubt the time is ripe for a dependent eliminator.

1 0