March 2013 - Libraries

RE: new-typeable, new cast?
by Simon Peyton-Jones 04 Mar '13

04 Mar '13

ok good. Since this is in the intersection of singletons and Typeable, I wonder if Pedro and Richard might together lead on driving this to a conclusion and implementing it? Simon | -----Original Message----- | From: Stephanie Weirich [mailto:sweirich@cis.upenn.edu] | Sent: 04 March 2013 14:24 | To: Shachaf Ben-Kiki | Cc: Simon Peyton-Jones; libraries(a)haskell.org; Richard Eisenberg | (eir(a)cis.upenn.edu) Dimitrios Vytiniotis; Iavor Diatchki; Conor | McBride; Pedro Magalhães | Subject: Re: new-typeable, new cast? | | Nice! I agree that having a (poly-kinded!) function of type | | >> eqT :: forall (a :: k) (b :: k). (Typeable a, Typeable b) => Maybe (a | >> :~: b) | | around is The Right Way to Go. I'd call this function "eqT" or | "eqTypeable", after the similar operation in Data.Type.Equality. Thanks | for pointing out that we can get such a function so easily from gcast. | (Note that gcast itself can be polykinded now, I'm writing down the | kinds to make them obvious.) | | gcast :: forall (a :: k) (b::k) (c::k ->*). (Typeable a, Typeable b) -> | c a -> Maybe (c b) | | WRT to gcast1 and gcast2, these functions can be subsumed by eqT, but | not by polykinded gcast due to the restrictions on higher-order | polymorphism. | | gcast1 can convert [b Int] to [Maybe Int], but gcast cannot. eqT can do | so with a pattern match. This behavior does seem rather special-purpose | though---eqT is much more flexible. | | With singletons, we could imagine two different polykinded operations, | that differ only in whether their arguments are explicit/implicit. | | eqTypeable :: (Typeable a, Typeable b) => Maybe (a :~: b) | | eqSing :: Sing a -> Sing b -> Maybe (a :~: b) | | Again, Sing should be kind-indexed, so that we can have Sing True, Sing | 0, and (eventually) Sing Int. | | --Stephanie | | | On Mar 4, 2013, at 8:46 AM, Shachaf Ben-Kiki wrote: | | > On Mon, Mar 4, 2013 at 4:24 AM, Simon Peyton-Jones | > <simonpj(a)microsoft.com> wrote: | >> | λ> data a :~: b where Refl :: a :~: a | >> | λ> :t gcast Refl | >> | gcast Refl :: forall a b. (Typeable a, Typeable b) => Maybe | >> | ((:~:) * a b) | >> | >> That is a ferociously-unintuitive use of 'gcast'! It too me dome | while to convince myself that it was right. Though it does indeed | work. I'd see (gcast Refl) as the primitive, with 'gcast' itself as a | simple derived function. | >> | >> I'm not sure what name to give the new cast function | >> ?? :: Typeable a, Typeable b) => Maybe (a :~: b) | >> | >> | >> Do we need gcast1 and gcast2 any more, in our new polykinded world? | Can they be depreceated? | >> | >> Simon | >> | > | > A couple of people have suggested "same". (I wonder if this would also | > subsume eqSingNat/eqSingSym?). | > | > By the way -- since (:~:) seems to be in HEAD now, but not yet | > released, is there a chance of renaming it? ":~:" is pretty awkward to | > type, given all the new TypeOperators options these days; how about | > "=="? | > | > Shachaf | >

2 1

new-typeable, new cast?
by Shachaf Ben-Kiki 04 Mar '13

04 Mar '13

This came up in #haskell -- rather than just provide coerce, cast (or a primitive that cast can be built on, as well as other things) can give a type equality witness of some kind. Some possible signatures are: cast :: (Typeable a, Typeable b) => Maybe (p a -> p b) -- Leibniz-style equality cast :: (Typeable a, Typeable b) => p a -> Maybe (p b) -- another form cast :: (Typeable a, Typeable b) => Maybe (Is a b) -- GADT-style equality cast :: (Typeable a, Typeable b) => MightBe a b -- another form -- With data Is a b where { Refl :: Is a a } -- standard equality GADT data MightBe a b where -- version with built-in Maybe, for more convenient types Is :: MightBe a a Isn't :: MightBe a b Any of these lets you write any of the other ones, of course. But "cast" doesn't let you write any of them, because it only goes in one direction. The GADT form can let you write code like foo :: forall a. Typeable a => a -> ... foo x | Is <- cast :: MightBe a Int = ...x... | Is <- cast :: MightBe a Char = ...x... | otherwise = ... Without coming up with a new name for x. It's possible to provide other functions on top of this primitive, like cast :: (Typeable a, Typeable b) => proxy a -> qroxy b -> ... -- to save some type annotations cast :: (Typeable a, Typeable b) => (a ~ b => r) -> Maybe r -- to use an expression directly cast :: (Typeable a, Typeable b) => a -> Maybe b -- the original Of the primitives I mentioned, the first two are H2010. The last two are nice to use directly, but use extensions (this probably doesn't matter so much for new-typeable). The Maybe form lets you say things like `fmap (\Is -> ...) (cast :: ...)` -- unfortunately, there's no "proper" Is type in base right now. The fourth version might save some typing, and might be slightly better performance-wise, since it saves a ⊥ (it's just represented like Bool at runtime)? Probably it all gets inlined so that doesn't matter anyway. Regardless of which particular primitive is used, it would be great for new-typeable to provide something stronger than cast. Shachaf

3 6

Continuous builds for bytestring
by Bryan O'Sullivan 03 Mar '13

03 Mar '13

We now run the build and test suite after every push to github. If something breaks, I'll be nagged. You'll need to click through a self-signed SSL cert warning from your browser: https://jenkins.serpentine.com/job/bytestring/

4 4

ANN: sandi 0.2 - reasonbly fast data encoding library
by Magnus Therning 02 Mar '13

02 Mar '13

I've just uploaded sandi version 0.2[1] to Hackage. Sandi is a data encoding library. It's aimed to be the successor of dataenc, my old data encoding library. Currently the following encodings are supported: - base16 - base32 - base32 hex - base64 - base64 url - base85 - quoted printable - uu - xx - yenc The main changes since the previous release: - Added benchmarks using criterion. - Modified API to make it better suited for piecemeal decoding by making decoding of base16, qp, and yenc accept correct but incomplete input. - Add a completely new API to allow using sandi with conduit. [1]: http://hackage.haskell.org/package/sandi-0.2 -- Magnus Therning OpenPGP: 0xAB4DFBA4 email: magnus(a)therning.org jabber: magnus(a)therning.org twitter: magthe http://therning.org/magnus

1 0