July 2012 - Haskell-Cafe

Re: [Haskell-cafe] sample terms and interpreting program output from Tc Monad
by Andres Löh 09 Jul '12

09 Jul '12

[Sorry, I forgot to reply to the list.] Hi. > I understand these to be Rank 0 terms: > > (\(x::Int) . x) (0 :: Int) :: (forall. Int) -- value > > (\(x::Int). x) :: (forall. Int -> Int) Yes. > (\(x::a). x) :: (forall. a -> a) > > Although the program prints forall, the absence of a type variable > indicates Rank 0, correct? It's a bit unclear what you mean, and the prototype implementation you seem to be using deviates from Haskell conventions here. The prototype checker sees "a" as a type constant here, so it plays the same role as "Int" before. In particular, "a" isn't a type variable, and there's no quantification. > I understand these to be Rank 1 terms: > > (\x. x) :: (forall a. a -> a) -- This is not the same as the third > example above, right? This one identifies the type variable a, the one > above does not. Also, there's no explicit annotation, it's inferred. The implementation indeed considers them to be different. Before "a" was a concrete type, and the function was the monomorphic identity function on that type. Now, "a" is a type variable, and the function is the polymorphic identity function. [...] > I understand these to be Rank 2 terms: > > (\(x::(forall a. a)). 0) :: (forall. (forall a. a) -> Int) > > The explicit forall annotation on the bound and binding variable x > causes the program to infer a Rank 2 polytype as indicated by the "-> > Int" following the (forall a. a), while noting the absence of a type > variable following the left-most forall printed by the program, correct? Your description here is a bit strange. It's a rank-2 type because there's a rank-1 type occurring to the left of the function arrow. > > (\(x::(forall a. a -> a)). x) :: (forall b. (forall a. a -> a) -> b -> > b) > > Also Rank 2, only one arrow to the right of (forall a. a -> a) counts. It's rank 2, yes. I'm not sure what you mean here by saying that only one arrow counts. > The universal quantifier on type variable b ranges over the type > variable a, correct? No. The universal quantifier ranges over all (mono)types. > I understand this to be a Rank 3 term: > > (\(f::(forall a. a -> a)). \(x::(forall b. b)). f (f x)) :: (forall c. > (forall a. a -> a) -> (forall b. b) -> c) No, this is still rank 2. It uses two rank 1 types as function arguments. For it to be rank 3, it'd have to use a rank 2 type in the argument position of a function type. Note that the function arrow associates to the right: forall c. (forall a. a -> a) -> ((forall b. b) -> c) -- rank 2 (forall c. ((forall a. a -> a) -> (forall b. b)) -> c) -- rank 3 > The arrows to the right of the universally quantified a and b > expressions qualify this as Rank 3. No, you seem to be applying a wrong definition of rank. The correct definition is given in Section 3.1 of the paper. Here's how you can derive the type above as a sigma_2: sigma_2 ~> forall c. sigma_2 ~> forall c. sigma_1 -> sigma_2 ~> forall c. sigma_1 -> sigma_1 -> sigma_2 ~> forall c. sigma_1 -> sigma_1 -> sigma_1 ~> forall c. sigma_1 -> sigma_1 -> sigma_0 ~> forall c. sigma_1 -> sigma_1 -> c ~> forall c. (forall a. sigma_1) -> sigma_1 -> c ~> forall c. (forall a. sigma_0) -> sigma_1 -> c ~> forall c. (forall a. tau -> tau) -> sigma_1 -> c ~> forall c. (forall a. a -> a) -> sigma_1 -> c ~> forall c. (forall a. a -> a) -> (forall b. sigma_1) -> c ~> forall c. (forall a. a -> a) -> (forall b. sigma_0) -> c ~> forall c. (forall a. a -> a) -> (forall b. b) -> c > Type variable c ranges over type > variables a and b, correct? No. Each of the type variables ranges over all (mono)types. (Or do you mean what the scope of "c" is? If so, then the scope of c is the complete type signature.) Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com

1 0

Interest in typed relational algebra library?
by Paul Visschers 08 Jul '12

08 Jul '12

Hello, I've been out of the Haskell game for a bit, but now I'm back. A couple of years ago I made a small library that implements relational algebra with types so that malformed queries and other operations are caught at compile time. It is heavily based off of the internals of HaskellDB (see http://hackage.haskell.org/packages/archive/haskelldb/2.1.1/doc/html/Databa…) but types so that it can actually be used directly instead of having to use HaskellDB's query monad. Besides the joy of using relational algebra directly in your code, this also means that you can make query-optimizing code in a type-safe way, you can subquery results returned by the database directly without accessing the database again and you have more options when converting from relation algebra to SQL or another query language. The library isn't quite ready for release, but I might want to work on it a bit and then release it. Is anyone interested in such a library? Paul Visschers

6 5

Haskell User Group Hamburg (Germany) - Meeting Thursday July 12th 2012
by Stefan Schmidt 08 Jul '12

08 Jul '12

Hello cafe, there's an upcomming meeting of the Haskell user group Hamburg next Thursday (July 12th). We'll start 19:00 at the Xing AG in Hamburg (Dammtorstraße 35, 20354 Hamburg ). Jan Ahrens will give a short talk about web development with Yesod ( http://www.yesodweb.com/) Although this announcement is written in english the talk will be given in german. If you are interested to join us, have a look at our doodle (also in german) http://www.doodle.com/5ekivcacuam9czxs Further announcements will be made via Twitter, so you may want to follow https://twitter.com/hug_hh.

1 0

vector-simd: some code available, and some questions
by Nicolas Trangez 08 Jul '12

08 Jul '12

All, After my message of yesterday [1] I got down to it and implemented something along those lines. I created a playground repository containing the code at [2]. Initial benchmark results at [3]. More about the benchmark at the end of this email. First some questions and requests for help: - I'm stuck with a typing issue related to 'sizeOf' calculation at [4]. I tried a couple of things, but wasn't able to figure out how to fix it. - I'm using unsafePerformIO at [5], yet I'm not certain it's OK to do so. Are there better (safer/performant/...) ways to get this working? - Currently Alignment phantom types (e.g. A8 and A16) are not related to each other: a function (like Data.Vector.SIMD.Algorithms.unsafeXorSSE42) can have this signature: unsafeXorSSE42 :: Storable a => SV.Vector SV.A16 a -> SV.Vector SV.A16 a -> SV.Vector SV.A16 a Yet, imaging I'd have an "SV.Vector SV.A32 Word8" vector at hand, the function should accept it as well (a 32-byte aligned vector is also 16-byte aligned). Is there any way to encode this at the type level? That's about it :-) As of now, I only implemented a couple of the vector API functions (the ones required to execute my benchmark). Adding the others should be trivial. The benchmark works with Data.Vector.{Unboxed|Storable}.Vector (UV and SV) vectors of Word8 values, as well as my custom Data.Vector.SIMD.Vector type (MV) using 16-byte alignment (MV.Vector MV.A16 Word8). benchUV, benchSV and benchMV all take 2 pre-calculated Word8 vectors of given size (1024 and 4096) and xor them pairwise into the result using "zipWith xor". benchMVA takes 2 suitable MV vectors and xor's them into a third using a rather simple and unoptimized C implementation using SSE4.2 intrinsics [6]. This could be enhanced quite a bit (I guess using the prim calling convention, FFI overhead can be reduced as well). Currently, only vectors of a multiple of 32 bytes are supported (mostly because of laziness on my part). As you can see, the zipWith Data.Vector.SIMD implementation is slightly slower than the Data.Vector.Storable based one. I didn't perform much profiling yet, but I suspect allocation and ForeignPtr creation is to blame, this seems to be highly optimized in GHC.ForeignPtr.mallocPlainForeignPtrBytes as used by Data.Vector.Storable. Thanks for any input, Nicolas [1] http://www.haskell.org/pipermail/haskell-cafe/2012-July/102167.html [2] https://github.com/NicolasT/vector-simd/ [3] http://linode2.nicolast.be/files/vector-simd-xor1.html [4] https://github.com/NicolasT/vector-simd/blob/master/src/Data/Vector/SIMD/Al… [5] https://github.com/NicolasT/vector-simd/blob/master/src/Data/Vector/SIMD/Al… [6] https://github.com/NicolasT/vector-simd/blob/master/cbits/vector-simd.c#L47

3 10

Which mailing list for GHC hacking discussion?
by Erik de Castro Lopo 08 Jul '12

08 Jul '12

Hi all, For GHC development questions (ie hacking on GHC, not with GHC) which is the appropriate mailing list ghc-cvs or ghc-users? Cheers, Erik -- ---------------------------------------------------------------------- Erik de Castro Lopo http://www.mega-nerd.com/

1 0

sample terms and interpreting program output from Tc Monad
by rickmurphy 07 Jul '12

07 Jul '12

Hi All: I'm still working through the following paper [1] and I wondered whether you could help me confirm my understanding of some sample terms and program output from the Tc Monad. For those interested, the language is specified in Parser.lhs available in the protoype here [2]. I understand these to be Rank 0 terms: (\(x::Int) . x) (0 :: Int) :: (forall. Int) -- value (\(x::Int). x) :: (forall. Int -> Int) (\(x::a). x) :: (forall. a -> a) Although the program prints forall, the absence of a type variable indicates Rank 0, correct? I understand these to be Rank 1 terms: (\x. x) :: (forall a. a -> a) -- This is not the same as the third example above, right? This one identifies the type variable a, the one above does not. Also, there's no explicit annotation, it's inferred. (\x. \y. x) :: (forall a b. b -> a -> b) -- Still rank 1. Although there's no explicit annotation, the program infers the type variables and prints the forall and the appropriate type variables for the Rank 1 polytypes. I understand these to be Rank 2 terms: (\(x::(forall a. a)). 0) :: (forall. (forall a. a) -> Int) The explicit forall annotation on the bound and binding variable x causes the program to infer a Rank 2 polytype as indicated by the "-> Int" following the (forall a. a), while noting the absence of a type variable following the left-most forall printed by the program, correct? (\(x::(forall a. a -> a)). x) :: (forall b. (forall a. a -> a) -> b -> b) Also Rank 2, only one arrow to the right of (forall a. a -> a) counts. The universal quantifier on type variable b ranges over the type variable a, correct? I understand this to be a Rank 3 term: (\(f::(forall a. a -> a)). \(x::(forall b. b)). f (f x)) :: (forall c. (forall a. a -> a) -> (forall b. b) -> c) The arrows to the right of the universally quantified a and b expressions qualify this as Rank 3. Type variable c ranges over type variables a and b, correct? Thanks for your help in better understanding this information. I'm home schooling myself on Haskell and community support is a big help. 1. Practical Type Inference for Arbitrary-Rank Types. 2.http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/ -- Rick

1 0

Odd HDBC connection bug
by William Shackleton 07 Jul '12

07 Jul '12

Hi I'm having issues with HDBC when connecting to a remote MySQL server - certain queries cause the DB connection to be lost. The following program demonstrates this: import Database.HDBC import Database.HDBC.ODBC main = do conn <- connectODBC "DSN=owlro" putStrLn "Connected" quickQuery' conn "SELECT time, power FROM Power LIMIT 100;" [] putStrLn "Finished query 1" quickQuery' conn "SELECT time, power FROM Power ORDER BY time;" [] putStrLn "Finished query 2" disconnect conn The DSN points to a remote 32-bit Ubuntu 12.04 Server. The connection and queries work using mysql and isql on the command line, and the table in question contains about 1.3 million rows and only the columns id, time, power. When I compile and run this on a 64-bit Ubuntu 12.04 PC using HDBC-2.3.1.1 and HDBC-odbc-2.3.1.0 using GHC, I get the following (unwanted) output: $ ghc Test.hs $ ./Test Connected Finished query 1 Test: SqlError {seState = "[\"08S01\"]", seNativeError = -1, seErrorMsg = "execute execute: [\"2013: [MySQL][ODBC 5.1 Driver][mysqld-5.5.24-0ubuntu0.12.04.1]Lost connection to MySQL server during query\"]"} This program finishes (and fails) in less than half a second. When I run it using runhaskell however, the slow second query completes: $ runhaskell Test.hs Connected Finished query 1 Finished query 2 I get the same result from ghci; this method takes about 10 seconds as expected. Basically, simple (short) queries complete, yet long ones crash the connection. I also noticed similar results with HDBC-mysql. Any ideas on what is causing this? Thanks, Will Shackleton digitalsquid.co.uk

1 1

ANNOUNCE: lens-family-th 0.1.0.0
by Dan Burton 07 Jul '12

07 Jul '12

Following the announcement of lens-family, I'm pleased to announce lens-family-th 0.1.0.0, a Template Haskell library supplying macros to generate lens-family lenses for fields of data types declared with record syntax. Be warned that currently, type signatures are *not* generated alongside the lens definitions. Type inference should correctly determine the type of the generated lenses, but I have structured the library code so that in the future, type signatures can also be generated. Patches welcome! http://hackage.haskell.org/package/lens-family-th -- Dan Burton

3 5

Re: [Haskell-cafe] translation between two flavors of lexically-scoped type variables
by oleg＠okmij.org 07 Jul '12

07 Jul '12

Kangyuan Niu wrote: > Aren't both Haskell and SML translatable into System F, from which > type-lambda is directly taken? The fact that both Haskell and SML are translatable to System F does not imply that Haskell and SML are just as expressive as System F. Although SML (and now OCaml) does have what looks like a type-lambda, the occurrences of that type lambda are greatly restricted. It may only come at the beginning of a polymorphic definition (it cannot occur in an argument, for example). > data Ap = forall a. Ap [a] ([a] -> Int) > Why isn't it possible to write something like: > > fun 'a revap (Ap (xs : 'a list) f) = f ys > where > ys :: 'a list > ys = reverse xs > > in SML? This looks like a polymorphic function: an expression of the form /\a.<body> has the type forall a. <type>. However, the Haskell function > revap :: Ap -> Int > revap (Ap (xs :: [a]) f) = f ys > where > ys :: [a] > ys = reverse xs you meant to emulate is not polymorphic. Both Ap and Int are concrete types. Therefore, your SML code cannot correspond to the Haskell code. That does not mean we can't use SML-style type variables (which must be forall-bound) with existentials. We have to write the elimination principle for existentials explicitly {-# LANGUAGE ExistentialQuantification, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} data Ap = forall a. Ap [a] ([a] -> Int) -- Elimination principle deconAp :: Ap -> (forall a. [a] -> ([a] -> Int) -> w) -> w deconAp (Ap xs f) k = k xs f revap :: Ap -> Int revap ap = deconAp ap revap' revap' :: forall a. [a] -> ([a] -> Int) -> Int revap' xs f = f ys where ys :: [a] ys = reverse xs Incidentally, GHC now uses SML-like design for type variables. However, there is a special exception for existentials. Please see 7.8.7.4. Pattern type signatures of the GHC user manual. The entire section 7.8.7 is worth reading.

2 2

Parameterized constraints
by Emil Axelsson 07 Jul '12

07 Jul '12

Hi! The `constraints` package provides ways to manipulate objects of kind `Constraint`. I need the same kind of manipulation, except that I need to work with objects of kind `* -> Constraint`. I.e. I need parameterized constraints that can be applied to different types. BTW, is there a standard term for things of kind `* -> Constraint`? I have a type family type family Constr (f :: * -> *) :: * -> Constraint which returns a parameterized constraint with the property that any value of type `f a` fulfills the constraint `Constr f a`. Since the constraint can be stronger than needed, I need something similar to `:-` from `constraints`, except it should operate on parameterized constraints. I have implemented the stuff I need (see below), but my question is if it's possible to do this with the `constraints` package directly (e.g. using `Forall`). I'm afraid I can't see how. Here is what I've come up with so far: -- Instead of (c1,c2) class (c1 a, c2 a) => (c1 :/\: c2) a instance (c1 a, c2 a) => (c1 :/\: c2) a -- Instead of (:-) type sub :< sup = forall a . Dict (sup a) -> Dict (sub a) -- Instead of weaken1 weak1 :: c1 :< (c1 :/\: c2) weak1 Dict = Dict weak2 :: c2 :< (c1 :/\: c2) weak2 Dict = Dict Thanks! -- / Emil

1 0