News aggregator

Problem using Text.Regex on OS X.

libraries list - Mon, 01/26/2015 - 1:29am
Hi, I'm new to Haskell so I'm not sure how to solve this issue, yet. I was directed to this list from the IRC channel. Here's the issue: Using GHCi on OS X: Prelude Data.Text> :m Text.Regex Prelude Text.Regex> let r = mkRegex "_" ... eliding successful "Loading package ..." lines ... Loading package regex-compat-0.95.1 ... can't load .so/.DLL for: /Library/Haskell/ghc-7.8.3-x86_64/lib/regex-compat-0.95.1/libHSregex-compat-0.95.1-ghc7.8.3.dylib (dlopen(/Library/Haskell/ghc-7.8.3-x86_64/lib/regex-compat-0.95.1/libHSregex-compat-0.95.1-ghc7.8.3.dylib, 9): Library not loaded: < at >rpath/libHSmtl-2.1.3.1-ghc7.8.3.dylib Referenced from: /Library/Haskell/ghc-7.8.3-x86_64/lib/regex-compat-0.95.1/libHSregex-compat-0.95.1-ghc7.8.3.dylib Reason: image not found) After running otool over the regex-compat dylib I can see lines like: ... Load command 24 cmd LC_RPATH cmdsize 80 path /Users/mark/Projects/hp/build/package/mtl-2.1.3.1/build/dist/build (offset 12) ... Which is not a path that is
Categories: Offsite Discussion

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

Haskell on Reddit - Sun, 01/25/2015 - 7:28pm

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]
Categories: Incoming News

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

Haskell on Reddit - Sun, 01/25/2015 - 3:48pm

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 pNorm

Which 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 t

Which would work, more or less, like this:

> solve x * 2 == 6 for x 3 > solve [1, 2, 3] == [1, x * 2, 3] for x 1

With 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 t

Without having to do the math manually. Or, even better, I could actually write all of my intersection functions at once:

hitSurface (ImplicitSurface b) => Ray a -> b -> [Point] hitSurface (Ray rPos rDir) surface = rayPoint ray t where t = solve (isInsideSurface (rPos + rDir * t) surface) for t

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?

submitted by SrPeixinho
[link] [17 comments]
Categories: Incoming News

ANN: snaplet-purescript

Haskell on Reddit - Sun, 01/25/2015 - 2:29pm
Categories: Incoming News

Unable to build 7.10.1 RC1 on Jessie

glasgow-user - Sun, 01/25/2015 - 12:18pm
I'm trying to build 7.10.1 RC on Debian Jessie. I get an error: configure: error: in `/ghc-7.10.0.20141222/libffi/build/x86_64-unknown-linux-gnu': configure: error: C++ preprocessor "/lib/cpp" fails sanity check config.log shows: configure: failed program was: | /* confdefs.h */ | #define PACKAGE_NAME "libffi" | #define PACKAGE_TARNAME "libffi" | #define PACKAGE_VERSION "3.1" | #define PACKAGE_STRING "libffi 3.1" | #define PACKAGE_BUGREPORT "http://github.com/atgreen/libffi/issues" | #define PACKAGE_URL "" | #define PACKAGE "libffi" | #define VERSION "3.1" | #define STDC_HEADERS 1 | #define HAVE_SYS_TYPES_H 1 | #define HAVE_SYS_STAT_H 1 | #define HAVE_STDLIB_H 1 | #define HAVE_STRING_H 1 | #define HAVE_MEMORY_H 1 | #define HAVE_STRINGS_H 1 | #define HAVE_INTTYPES_H 1 | #define HAVE_STDINT_H 1 | #define HAVE_UNISTD_H 1 | #define HAVE_DLFCN_H 1 | #define LT_OBJDIR ".libs/" | /* end confdefs.h. */ | #ifdef __STDC__ | # include <limits.h> | #else | # include <assert.h> | #endif | Syntax er
Categories: Offsite Discussion

Yesod Web Framework: PolyConf 2015

Planet Haskell - Sun, 01/25/2015 - 7:30am

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.

Categories: Offsite Blogs

Haskell web site is really, *really* slow.

Haskell on Reddit - Sun, 01/25/2015 - 4:49am

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]
Categories: Incoming News

Dominic Steinitz: A Type Safe Reverse or Some Hasochism

Planet Haskell - Sun, 01/25/2015 - 3:07am

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.Proxy

The usual natural numbers:

> data Nat = Z | S Nat

We need some axioms:

  1. A left unit and
  2. Restricted commutativity.
> type family (n :: Nat) :+ (m :: Nat) :: Nat where > Z :+ m = m > S n :+ m = n :+ S m

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)) Refl

This 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
  1. S Z :+ n2 = Z :+ S n2 (by axiom 2) = S n2 (by axiom 1) and
  2. S (Z + n2) = S n2 (by axiom 1)
  3. So S Z :+ n2 = S (Z + n2)
  • For SSucc
  1. SSucc n :: SNat (S k) so n :: SNat k and m :: SNat i so SSucc m :: SNat (S i)
  2. succ_plus id n (SSucc m) :: k ~ S p => S p :+ S i :~: S (p :+ S i) (by hypothesis)
  3. k ~ S p => S p :+ S i :~: S (S p :+ i) (by axiom 2)
  4. k :+ S i :~: S (k :+ i) (by substitution)
  5. 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
  1. Z :+ Z = Z (by axiom 1)
  • For SSucc
  1. SSucc n :: SNat (S k) so n :: SNat k
  2. plus_id_r n :: k :+ Z :~: k (by hypothesis)
  3. succ_plus_id n SZero :: S k :+ Z :~: S (k + Z) (by the succ_plus_id lemma)
  4. succ_plus_id n SZero :: k :+ Z ~ k => S k :+ Z :~: S k (by substitution)
  5. 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) x

Armed 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) Refl

For 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) Refl

Now 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"] Bibliography

Lambek, 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.


Categories: Offsite Blogs

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

Planet Haskell - Sun, 01/25/2015 - 2:50am

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!


Categories: Offsite Blogs

Monad layering and DSL

haskell-cafe - Sat, 01/24/2015 - 8:46pm
Hello all, I'm trying to make an IMAP DSL and I'm face to an annoying issue (all the examples after are selected pieces of this: https://github.com/blackheaven/smoothmail). Here we are, IMAP provide a way to statefully interact with a server. For example: select "A" -- Select folder 'A' searchAll -- Get the list of UID (message identifiers) [1, 2, 3] But select "B" searchAll -- Get [4, 5] I decided to use the Free Monad because it seems well suite for what I'm doing and I end-up with something like that: data ImapF next = Select DirectoryName (Maybe DirectoryDescription -> next) | Noop (DirectoryDescription -> next) | Search MailSearch (Maybe [UID] -> next)
Categories: Offsite Discussion

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

Haskell on Reddit - Sat, 01/24/2015 - 3:54pm
  • 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.

submitted by chromaticburst
[link] [5 comments]
Categories: Incoming News

thoughtbot/til

del.icio.us/haskell - Sat, 01/24/2015 - 12:04pm
Categories: Offsite Blogs