- Libraries - Haskell.org

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 02 Nov '16

02 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 02 Nov '16

02 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

Proposal: Add Data instance for Const
by Ryan Scott 02 Nov '16

02 Nov '16

GHC Trac #12438 [1] exists because there's no Data instance for Const in base. I found this quite surprising, since we have Data instances for just about every other type combinator out there (Identity, Sum, Product, Compose, etc.), but not for Const. The fix for #12438 would be quite simple: I propose we add deriving instance (Data a, Data b) => Data (Const a b) to Data.Data in base. Any objections? Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/ticket/12438

4 6

Re: Type Level "Application" Operator
by Ryan Scott 02 Nov '16

02 Nov '16

> But this makes me wonder, is it actually *impossible* in Haskell to export from the same module a function with the same name at both the value and type level? Is it possible to export only one of the two? It's quite possible. You just have to use the "type" namespace in your export list to disambiguate the term-level and type-level ($)s: {-# LANGUAGE TypeOperators #-} module Money (($), type ($)) where type f $ x = f x infixr 0 $ Also, +1 on the original suggestion to add ($) to base. Ryan S.

1 0

Re: Few changes to deepseq
by Ryan Scott 27 Oct '16

27 Oct '16

All three of those proposals seem useful, broadly applicable, and sensibly named, so +1 from me. Ryan S.

1 0