# News aggregator

### ANN: deepseq-bounded 0.5 -> 0.6

### Problem using Text.Regex on OS X.

### ANN: Halcyon and Haskell on Heroku

### existentials + typeclasses, variants, and "open-world" generic heterogeneous data structures

Hi, r/haskell!

I've been working in Haskell for the past year or so, and have come to appreciate its beauty and simplicity more the more I use it. But I've come on a problem that has me a little stymied.

I'm building a DSL library that I want to be extensible, i.e., that the user can add new primitives to. The DSL library will allow "objects" to be in scope (held by a state object part of the DSL monad) and will provide combinators that allow for control flow in the DSL, such as if/else and looping. The objects have a set of well-defined operations: "predicate" (conditionalize the object down one branch of an if/else), "join" (join two branches of the object value at a control-flow merge point), and "generate" (generate the IR).

The problem comes in how to allow these objects to be stored in the core data structure (the environment state in the DSL monad). At its most basic level, it's a heterogeneous list (or map). I started by using an existential type for this, wrapping a typeclass:

data DSLState = DSLState { dslstateEnv :: Data.Map.Map ObjectID Object, ... } data Object = forall a. Object_ a class Object_ a where objID :: a -> ObjectID objPredicate :: a -> PredicateCondition -> a objJoin :: a -> a -> a objGenerate :: a -> (IR parameters and result)But clearly this doesn't work because, e.g., the second argument of objJoin, and the return type of objPredicate and objJoin, are a, not Object. In the combinator implementations that need to invoke Predicate and Join, I have only Objects, and the existential hides the a type.

Moreover, I understand *why* the type system is giving me trouble here. There's no reason that the typechecker should trust that I pass the right object type as the second argument to objJoin. What if I try to join two objects of different types? The existential *should* disallow such an objJoin, for that reason.

The way I've gotten around this right now is to implement a Variant type (using unsafeCoerce and explicit integer type tags), and create a generic layer that uses only Variants (I also refactored out the typeclass+existential to a simple "curry the this pointer" manual dictionary-passing record, but I think that's orthogonal):

data Object = Object { objID :: ObjectID, objDataType :: VariantID, objData :: Variant, -- impl uses unsafeCoerce objPredicate :: PredicateCondition -> Object, objJoin :: Object -> Object, objGenerate :: (IR parameters and result) }This is unnecessarily ugly, though, and requires boilerplate for every Object type. The standard existentials + typeclass example I see everywhere uses either UI widgets or shapes, but those problems never require another shape to appear on the RHS of any function type. Only the 'this' pointer (to borrow an OOP concept) is polymorphic.

One step in the right direction would be some sort of downcasting. E.g., a "downcast :: Object -> Maybe a" function. I attempted something like this with typeclasses but gave up after running into the non-overlapping restriction.

Another way out would be to give up on the "open world" requirement. If I could explicitly say "data Object = ObjectA ... | ObjectB ..." then I'd be done. But as this is a library, I'd rather leave it open to the user to add new object types.

Is there a standard solution to this? Or is there a name for the problem? Is there some trick I can use to reduce boilerplate?

Thanks!

submitted by cfallin[link] [4 comments]

### "Solve _ for _" expression: any study on this (or similar) ideas?

For a geometry library in Haskell, I had to write several ray-surface intersection functions such as:

intersectRayPlane :: Ray → Plane → [Point] intersectRaySphere :: Ray → Sphere → [Point] intersectRayTrig :: Ray → Trig → [Point] intersectRayBox :: Ray → Box → [Point] intersectRayCone :: Ray → Cone → [Point] (...)Soon enough, I noticed that this job was mostly repetitive. In order to implement a new intersection function, I had to do, precisely, do the following tasks:

1. Write down the implicit equation for the surface (ex: `x^2 + y^2 + z^2 = r^2`, for a sphere). 2. Substitute the ray equation on them: `rayPoint t = pos + dir * t` 3. Solve for t. I will have an equation such as: `t = stuff`. 4. Write that on Haskell, in the form: `hitSphere (Ray pos dir) sphere = pos + dir * t where t = stuff`For example, here is my hitPlane function:

hitPlane :: (Num a, Fractional a) => Ray a -> Plane a -> [V3 a] hitPlane (Ray rPos rDir) (Plane pPos pNorm) = [rPos + t *^ rDir] where t = dot (pPos - rPos) pNorm / dot rDir pNormWhich was derived manually from this process. I started to wonder if I could - as with most manual labors - automatize this process on Haskell. Unfortunatelly, the answer is no, since it would need some kind of mechanism that is not available in Haskell:

solve equation for tWhich would work, more or less, like this:

> solve x * 2 == 6 for x 3 > solve [1, 2, 3] == [1, x * 2, 3] for x 1With such a feature, I could easily implement my hitPlane function as:

hitPlane (Ray rPos rDir) (Plane rPos pNorm) = rPos + t *^ rDir where t = solve (isInsideSphere (rPos + rDir * t)) for tWithout having to do the math manually. Or, even better, I could actually write **all of my intersection functions** at once:

Now, I completely understand this is **absurd** and **undecidable** in general. Netherless, programs such as Mathematica have similar solves which work perfectly, so, I wonder if something on those lines could be implemented, even if just as a limited compile-time macro with template haskell. Has this idea been studied already? What are the relevant papers/keywords?

[link] [17 comments]

### Awesome Cassandra library: cql-io

### A Type Safe Reverse or Some Hasochism

### Unable to build 7.10.1 RC1 on Jessie

### Yesod Web Framework: PolyConf 2015

Last year I spoke at PolyConf about client/server Haskell webapps, and especially on GHCJS. This year's PolyConf has just opened up a Call for Proposals.

I really enjoyed my time at the conference last year: it's a great place to meet and interact with people doing cool things in other languages, and can be a great source of inspiration for ways we can do things better. Also, as I've mentioned recently, I think it's a great thing for us Haskellers to put out content accessible by the non-Haskell world, and a conference like this is a perfect way to do so.

If you have a topic that you think polyglot programmers would be interested in, please take the time to submit a proposal for the conference.

### Haskell web site is really, *really* slow.

Seriously guys, it's embarrassing. Can someone replace the site with a static one until the backend is sorted out?

submitted by pja[link] [64 comments]

### Dominic Steinitz: A Type Safe Reverse or Some Hasochism

Conor McBride was not joking when he and his co-author entitled their paper about dependent typing in Haskell “Hasochism”: Lindley and McBride (2013).

In trying to resurrect the Haskell package yarr, it seemed that a dependently typed reverse function needed to be written. Writing such a function turns out to be far from straightforward. How GHC determines that a proof (program) discharges a proposition (type signature) is rather opaque and perhaps not surprisingly the error messages one gets if the proof is incorrect are far from easy to interpret.

I’d like to thank all the folk on StackOverflow whose answers and comments I have used freely below. Needless to say, any errors are entirely mine.

Here are two implementations, each starting from different axioms (NB: I have never seen type families referred to as axioms but it seems helpful to think about them in this way).

> {-# OPTIONS_GHC -Wall #-} > {-# OPTIONS_GHC -fno-warn-name-shadowing #-} > {-# OPTIONS_GHC -fno-warn-type-defaults #-} > {-# OPTIONS_GHC -fno-warn-unused-do-bind #-} > {-# OPTIONS_GHC -fno-warn-missing-methods #-} > {-# OPTIONS_GHC -fno-warn-orphans #-} > {-# LANGUAGE GADTs #-} > {-# LANGUAGE KindSignatures #-} > {-# LANGUAGE DataKinds #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE UndecidableInstances #-} > {-# LANGUAGE ExplicitForAll #-} > {-# LANGUAGE TypeOperators #-} > {-# LANGUAGE ScopedTypeVariables #-}For both implementations, we need propositional equality: if a :~: b is inhabited by some terminating value, then the type a is the same as the type b. Further we need the normal form of an equality proof: Refl :: a :~: a and a function, gcastWith which allows us to use internal equality (:~:) to discharge a required proof of external equality (~). Readers familiar with topos theory, for example see Lambek and Scott (1988), will note that the notation is reversed.

> import Data.Type.Equality ( (:~:) (Refl), gcastWith )For the second of the two approaches adumbrated we will need

> import Data.ProxyThe usual natural numbers:

> data Nat = Z | S NatWe need some axioms:

- A left unit and
- Restricted commutativity.

We need the usual singleton for Nat to tie types and terms together.

> data SNat :: Nat -> * where > SZero :: SNat Z > SSucc :: SNat n -> SNat (S n)Now we can prove some lemmas.

First a lemma showing we can push :+ inside a successor, S.

> succ_plus_id :: SNat n1 -> SNat n2 -> (((S n1) :+ n2) :~: (S (n1 :+ n2))) > succ_plus_id SZero _ = Refl > succ_plus_id (SSucc n) m = gcastWith (succ_plus_id n (SSucc m)) ReflThis looks nothing like a standard mathematical proof and it’s hard to know what ghc is doing under the covers but presumably something like this:

- For SZero

- S Z :+ n2 = Z :+ S n2 (by axiom 2) = S n2 (by axiom 1) and
- S (Z + n2) = S n2 (by axiom 1)
- So S Z :+ n2 = S (Z + n2)

- For SSucc

- SSucc n :: SNat (S k) so n :: SNat k and m :: SNat i so SSucc m :: SNat (S i)
- succ_plus id n (SSucc m) :: k ~ S p => S p :+ S i :~: S (p :+ S i) (by hypothesis)
- k ~ S p => S p :+ S i :~: S (S p :+ i) (by axiom 2)
- k :+ S i :~: S (k :+ i) (by substitution)
- S k :+ i :~: S (k :+ i) (by axiom 2)

Second a lemma showing that Z is also the right unit.

> plus_id_r :: SNat n -> ((n :+ Z) :~: n) > plus_id_r SZero = Refl > plus_id_r (SSucc n) = gcastWith (plus_id_r n) (succ_plus_id n SZero)- For SZero

- Z :+ Z = Z (by axiom 1)

- For SSucc

- SSucc n :: SNat (S k) so n :: SNat k
- plus_id_r n :: k :+ Z :~: k (by hypothesis)
- succ_plus_id n SZero :: S k :+ Z :~: S (k + Z) (by the succ_plus_id lemma)
- succ_plus_id n SZero :: k :+ Z ~ k => S k :+ Z :~: S k (by substitution)
- plus_id_r n :: k :+ Z :~: k (by equation 2)

Now we can defined vectors which have their lengths encoded in their type.

> infixr 4 ::: > data Vec a n where > Nil :: Vec a Z > (:::) :: a -> Vec a n -> Vec a (S n)We can prove a simple result using the lemma that Z is a right unit.

> elim0 :: SNat n -> (Vec a (n :+ Z) -> Vec a n) > elim0 n x = gcastWith (plus_id_r n) xArmed with this we can write an reverse function in which the length of the result is guaranteed to be the same as the length of the argument.

> size :: Vec a n -> SNat n > size Nil = SZero > size (_ ::: xs) = SSucc $ size xs > accrev :: Vec a n -> Vec a n > accrev x = elim0 (size x) $ go Nil x where > go :: Vec a m -> Vec a n -> Vec a (n :+ m) > go acc Nil = acc > go acc (x ::: xs) = go (x ::: acc) xs > toList :: Vec a n -> [a] > toList Nil = [] > toList (x ::: xs) = x : toList xs > test0 :: [String] > test0 = toList $ accrev $ "a" ::: "b" ::: "c" ::: Nil ghci> test0 ["c","b","a"]For an alternative approach, let us change the axioms slightly.

> type family (n1 :: Nat) + (n2 :: Nat) :: Nat where > Z + n2 = n2 > (S n1) + n2 = S (n1 + n2)Now the proof that Z is a right unit is more straightforward.

> plus_id_r1 :: SNat n -> ((n + Z) :~: n) > plus_id_r1 SZero = Refl > plus_id_r1 (SSucc n) = gcastWith (plus_id_r1 n) ReflFor the lemma showing we can push + inside a successor, S, we can use a Proxy.

> plus_succ_r1 :: SNat n1 -> Proxy n2 -> ((n1 + (S n2)) :~: (S (n1 + n2))) > plus_succ_r1 SZero _ = Refl > plus_succ_r1 (SSucc n1) proxy_n2 = gcastWith (plus_succ_r1 n1 proxy_n2) ReflNow we can write our reverse function without having to calculate sizes.

> accrev1 :: Vec a n -> Vec a n > accrev1 Nil = Nil > accrev1 list = go SZero Nil list > where > go :: SNat n1 -> Vec a n1 -> Vec a n2 -> Vec a (n1 + n2) > go snat acc Nil = gcastWith (plus_id_r1 snat) acc > go snat acc (h ::: (t :: Vec a n3)) = > gcastWith (plus_succ_r1 snat (Proxy :: Proxy n3)) > (go (SSucc snat) (h ::: acc) t) > test1 :: [String] > test1 = toList $ accrev1 $ "a" ::: "b" ::: "c" ::: Nil ghci> test0 ["c","b","a"] BibliographyLambek, J., and P.J. Scott. 1988. *Introduction to Higher-Order Categorical Logic*. Cambridge Studies in Advanced Mathematics. Cambridge University Press. http://books.google.co.uk/books?id=6PY_emBeGjUC.

Lindley, Sam, and Conor McBride. 2013. “Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming.” In *Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell*, 81–92. Haskell ’13. New York, NY, USA: ACM. doi:10.1145/2503778.2503786.

### Noam Lewis: Ok, Internet, I heard you. I need a new name for the JS type inferer/checker.

I knew a new name is needed for this JS type inferer/checker. Many people have pointed out that sweet.js uses the same short name (sjs). I could just stick with “Safe JS” but not make it short. Or I could pick a new name, to make it less boring.

Help me help you!

**Please take this quick poll.**

Thanks!

### Monad layering and DSL

### Uniform access to data in Haskell (exploring the "design space")

I apologize in advance if this is not well thought out. I'm posting here for guidance and conversation.

This is not a proposal for Haskell, just some fun ideas.

Smarter people than I have already had these ideas but I don't know the terminology (row types, extensible records, type level literals and dependent types?) so please link me to papers if you know where this has been covered. This paper by Daan Leijen was one I read.

Our motivation is uniform access to data (perhaps full CRUD). I'm very much a "completionist" so this made me sketch out how several of Haskell's "collections" are related. I came up with a "design space" (for lack of a better word) with 3 axes: RowTyped (yes|no), KeyType (Int|Symbol), Extensible (yes|no) = 2 * 2 * 2 = 8 and here is a terrible diagram of what I mean.

For read-only access we start with "class ReadMap k v where readData :: k -> Maybe v". Map already supports this and List can be made to support it when k = Int. Adding "deriving ReadMap" would add this to Data Constructors and Records comprised of only one type for Types with only one constructor. Meaning: data T = T Int Int deriving ReadMap, and data T = T {x = Int, y = Int} deriving ReadMap makes sense but obviously not data T = T Int String or data T = A Int | B String. For update access we add "updateData :: d -> k -> KeyNotFound | Updated d".

But how do we add this to "row typed" things (where I just mean things with a type like Tuple)? What if we could use literal values in types (without going into full Dependent Types)? Let's create a magic type signature: getData :: (x = Literal k) -> (r = RowType k) -> (r @ x). Where the type parameter for Literal will be either Nat or Symbol - because we already have these two in our existing Type Level Literals!

So we needed to add 4 things to the type system. A Literal type that hoists a literal up to the existing Nat and Symbol types, "=" notation for referencing a type level map or a value of a Literal, a "RowType key" type that is a type level map from Nat or Symbol keys to a type value, "@" notation for getting from the type level map.

Elm has extensible records. It's interesting to note his fear they will be abused to create Objects. The goal here isn't to make everying a map like in Lua and JS. Just to get access to tantalizingly close info that we already know at compile time but don't have the notation to express (indexable tuples). I purposely omitted insert and delete to keep this short.

**TLDR:** If we can: hoist integer and string literals to the existing type level literals + abstract the existing Tuple/Record types as a "type level map" from a Nat or Symbol key to a type + add notation for extracting values (types) from these type maps, then we have uniform read and update access to Lists, Maps, Tuples and Data/Records, as well as making these things indexable and keeping compile time type saftey.

[link] [5 comments]