News aggregator

Tagged instances for Aeson overlapped

haskell-cafe - Mon, 03/07/2016 - 4:37pm
Hello, I tried to compile my project with GHC 8 (from HEAD). And I got One of instances should be removed probably. I suppose that instance for removing should be instance in Data.Tagged. But version in Aeson should be PolyKinded. What do you think? Best regards, Dmitry _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe< at >haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Categories: Offsite Discussion

Trouble on Travis CI with recent cabal versions

haskell-cafe - Mon, 03/07/2016 - 10:19am
For my OpenGLRaw project, I'm using a .travis.yml generated by Herbert's https://github.com/hvr/multi-ghc-travis and the corresponding https://launchpad.net/~hvr/+archive/ubuntu/ghc PPA. Recently things broke on Travis CI, and there are a few strange things: * The cabal-install-head package seems to be based on cabal 1.23, which is older than cabal-install-1.24. Is this intended? * The OpenGLRaw package has no test suite, and this seems to be OK for cabal-install-head ( https://travis-ci.org/haskell-opengl/OpenGLRaw/jobs/114109605#L929), while cabal-install-1.24 fails in the "cabal test" step ( https://travis-ci.org/haskell-opengl/OpenGLRaw/jobs/114109606#L1022). This is a regression: I think that "cabal test" for a package without a test suite should be a no-op, at least that used to be the case. * Why does "cabal test" say "Re-configuring with test suites enabled. If this fails, please run configure manually." when "cabal configure" has already been run (including --enable-tests)? This looks li
Categories: Offsite Discussion

1-to-many preprocessor in stack/Cabal builds

haskell-cafe - Mon, 03/07/2016 - 8:53am
Hi, I'm writing a package which uses custom preprocessor for creating some of the source files. It takes one IDL file as input and writes several .hs modules, depending on IDL contents. I need to compile this modules with a few normal ones and link them as a library, preferably with generated modules exposed. It doesn't look like a complex task and never was in with make/etc, but I run into some problems now. Obviously, cabal supports 1-to-1 preprocessors to create one Haskell module from one source file (alex, happy, etc), but I can't find anything for 1-to-many preprocessors. So, I decided to use hookedPrograms and hooks and do it myself. The call to preprocessor in the postConf hook worked just fine and created source files and module list. Cabal pre-* hooks seems to be right place to read this module list and use it, but are presenting two problems: can only modify other-modules, not exposed-modules, which is tolerable, and there is no access to build configuration. The latter is fatal, I need to know
Categories: Offsite Discussion

PolyKind for Fixed and HasResolution from Data.Fixed

haskell-cafe - Sun, 03/06/2016 - 7:29pm
Hi all! If we define HasResolution and Fixed like that: class HasResolution (a :: k) where resolution :: p a -> Integer newtype Fixed (a :: k) = Fixed Integer We can do something like that: instance KnownNat a => HasResolution a where resolution = natVal 2.3 :: Fixed 1
Categories: Offsite Discussion

GADTs and Exponentiated Functors

haskell-cafe - Sun, 03/06/2016 - 2:11pm
Hi, I have been recently playing around with GADTs, using them to keep track of how many times a functor has been applied. This provides a solution to what seems to be a long standing problem, summarized here: https://byorgey.wordpress.com/2007/08/16/mapping-over-a-nested-functor/ If the nesting depth is part of the type, it is possible to apply fmap automatically as needed. This allows you to write fairly elegant expressions like: data Person = Person { name :: String, age :: Integer, gender :: String, status :: String } deriving Show let persons = fromList' [Person {name="Alice", age=20, gender="F", status="Good"}, Person {name="Bob", age=18, gender="M", status="Good"}, Person {name="Chuck", age=16, gender="M", status="Bad"}] :: NList N1 Person persons `select` age
Categories: Offsite Discussion

Philip Wadler: The Ask

Planet Haskell - Sun, 03/06/2016 - 9:40am
Scottish elections take place on 5 May 2016.

The Scottish Government have set a target of 10% of all trips by foot or bicycle, but less than 2% of the Scottish travel budget goes to 'active travel' (the buzzword for getting from one place to another minus a motor). We Walk, We Cycle, We Vote and Spokes suggest you ask your candidate to pledge the following:
To raise the share of the transport budget spent on walking and cycling to 10% over the course of the next parliament.See the pages linked above for more info, including hustings you can attend to put the question to your local candidates. A don't forget to Pedal on Parliament on 23 April 2016.


Categories: Offsite Blogs

Type-level list "elem" inference

haskell-cafe - Sat, 03/05/2016 - 9:34pm
So I've got some code that looks like: {-# LANGUAGE DataKinds, UndecidableInstances, TypeFamilies, KindSignatures, TypeOperators #-} import Data.Proxy import GHC.TypeLits type family IsSubset (as :: [Symbol]) (bs :: [Symbol]) where IsSubset as bs = IsSubsetPrime as bs bs type family IsSubsetPrime (as :: [Symbol]) bs bs' where IsSubsetPrime as '[] bs' = 'False IsSubsetPrime '[] bs bs' = 'True IsSubsetPrime (a ': as) (a ': bs) bs' = IsSubsetPrime as bs' bs' IsSubsetPrime (a ': as) (b ': bs) bs' = IsSubsetPrime (a ': as) bs bs' This lets me write functions like: foo :: (IsSubset '["foo", "bar"] args ~ 'True) => Proxy args -> Int foo args = undefined I've also got a type family: type family IsElem (a :: Symbol) (bs :: [Symbol]) where IsElem a (a ': bs) = 'True IsElem a (b ': bs) = IsElem a bs IsElem a '[] = 'False This lets me write functions like: bar :: (IsElem "foo" args ~ 'True) => Proxy args -> Int bar args = undefined The problem comes when I want to use "bar args"
Categories: Offsite Discussion

Gabriel Gonzalez: From mathematics to map-reduce

Planet Haskell - Sat, 03/05/2016 - 9:24pm

There's more mathematics to programming than meets the eye. This post will highlight one such connection that explains the link between map-reduce and category theory. I will then conclude with some wild speculation about what this might imply for future programming paradigms.

This post assumes that you already know Haskell and explains the mathematics behind the map-reduce using Haskell concepts and terminology. This means that this post will oversimplify some of the category theory concepts in order to embed them in Haskell, but the overall gist will still be correct.

Background (Isomorphism)

In Haskell, we like to say that two types, s and t, are "isomorphic" if and only if there are two functions, fw and bw, of types

fw :: s -> t
bw :: t -> s

... that are inverse of each other:

fw . bw = id
bw . fw = id

We will use the symbol ≅ to denote that two types are isomorphic. So, for example, we would summarize all of the above by just writing:

s ≅ t

The fully general definition of isomorphism from category theory is actually much broader than this, but this definition will do for now.

Background (Adjoint functors)

Given two functors, f and g, f is left-adjoint to g if and only if:

f a -> b ≅ a -> g b

In other words, for them to be adjoint there must be two functions, fw and bw of types:

fw :: (f a -> b) -> (a -> g b)
bw :: (a -> g b) -> (f a -> b)

... such that:

fw . bw = id
bw . fw = id

These "functors" are not necessarily the same as Haskell's Functor class. The category theory definition of "functor" is more general than Haskell's Functor class and we'll be taking advantage of that extra generality in the next section.

Free functors

Imagine a functor named g that acted more like a type-level function that transforms one type into another type. In this case, g will be a function that erases a constraint named C. For example:

-- `g` is a *type-level* function, and `t` is a *type*
g (C t => t) = t

In other words, g "forgets" the C constraint on type t. We call g a "forgetful functor".

If some other functor, f is left-adjoint to g then we say that f is the "free C" (where C is the constraint that g "forgets").

In other words, a "free C" is a functor that is left-adjoint to another functor that forgets the constraint C.

Free monoid

The list type constructor, [], is the "free Monoid"

The "free Monoid" is, by definition, a functor [] that is left-adjoint to some other functor g that deletes Monoid constraints.

When we say that g deletes Monoid constraints we mean that:

g (Monoid m => m) = m

... and when we say that [] is left-adjoint to g that means that:

[] a -> b ≅ a -> g b

... and the type [a] is syntactic sugar for [] a, so we can also write:

[a] -> b ≅ a -> g b

Now substitute b with some type with a Monoid constraint, like this one:

b = Monoid m => m

That gives us:

[a] -> (Monoid m => m) ≅ a -> g (Monoid m => m)

... and since g deletes Monoid constraints, that leaves us with:

[a] -> (Monoid m => m) ≅ a -> m

The above isomorphism in turn implies that there must be two functions, fw and bw, of types:

fw :: ([a] -> (Monoid m => m)) -> (a -> m)
bw :: (a -> m) -> ([a] -> (Monoid m => m))

... and these two functions must be inverses of each other:

fw . bw = id
bw . fw = id

We can pull out the Monoid constraints to the left to give us these more idiomatic types:

fw :: (Monoid m => [a] -> m)) -> (a -> m)
bw :: Monoid m => ( a -> m) -> ([a] -> m)

Both of these types have "obvious" implementations:

fw :: (Monoid m => [a] -> m)) -> (a -> m)
fw k x = k [x]

bw :: Monoid m => (a -> m) -> ([a] -> m)
bw k xs = mconcat (map k xs)

Now we need to prove that the fw and bw functions are inverse of each other. Here are the proofs:

-- Proof #1
fw . bw

-- eta-expand
= \k -> fw (bw k)

-- eta-expand
= \k x -> fw (bw k) x

-- Definition of `fw`
= \k x -> bw k [x]

-- Definition of `bw`
= \k x -> mconcat (map k [x])

-- Definition of `map`
= \k x -> mconcat [k x]

-- Definition of `mconcat`
= \k x -> k x

-- eta-reduce
= \k -> k

-- Definition of `id`
= id



-- Proof #2
bw . fw

-- eta-expand
= \k -> bw (fw k)

-- eta-expand
= \k xs -> bw (fw k) xs

-- Definition of `bw`
= \k xs -> mconcat (map (fw k) xs)

-- eta-expand
= \k xs -> mconcat (map (\x -> fw k x) xs)

-- Definition of `fw`
= \k xs -> mconcat (map (\x -> k [x]) xs)

-- map (f . g) = map f . map g
= \k xs -> mconcat (map k (map (\x -> [x]) xs))

-- ... and then a miracle occurs ...
--
-- In all seriousness this step uses a "free theorem" which says
-- that:
--
-- forall (k :: Monoid m => [a] -> m) . mconcat . map k = k . mconcat
--
-- We haven't covered free theorems, but you can read more about them
-- here: http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf
= \k xs -> k (mconcat (map (\x -> [x]) xs)

-- This next step is a proof by induction, which I've omitted
= \k xs -> k xs

-- eta-reduce
= \k -> k

-- Definition of `id`
= idMap reduce

Let's revisit the type and implementation of our bw function:

bw :: Monoid m => (a -> m) -> ([a] -> m)
bw k xs = mconcat (map k xs)

That bw function is significant because it is a simplified form of map-reduce:

  • First you "map" a function named k over the list of xs
  • Then you "reduce" the list using mconcat

In other words, bw is a pure "map-reduce" function and actually already exists in Haskell's standard library as the foldMap function.

The theory of free objects predict that all other functions of interest over a free object (like the free Monoid) can be reduced to the above fundamental function. In other words, the theory indicates that we can implement all other functions over lists in terms of this very general map-reduce function. We could have predicted the importance of "map-reduce purely from the theory of "free Monoids"!

However, there are other free objects besides free Monoids. For example, there are "free Monads" and "free Categorys" and "free Applicatives" and each of them is equipped with a similarly fundamental function that we can use to express all other functions of interest. I believe that each one of these fundamental functions is a programming paradigm waiting to be discovered just like the map-reduce paradigm.

Categories: Offsite Blogs

Magnus Therning: From JSON to sum type

Planet Haskell - Sat, 03/05/2016 - 6:00pm

For a while I’ve been planning to take full ownership of the JSON serialisation and parsing in cblrepo. The recent inclusion of instances of ToJSON and FromJSON for Version pushed me to take the first step by writing my own instances for all external types.

When doing this I noticed that all examples in the aeson docs use a product

data Person = Person { name :: Text , age :: Int }

whereas I had to deal with quite a few sums, e.g. VersionRange. At first I struggled a little with how to write an instance of FromJSON. After quite a bit of thinking I came up with the following, which I think is fairly nice, but I’d really like to hear what others think about it. Maybe I’ve just missed a much simpler way of implementing parseJSON:

instance FromJSON V.VersionRange where parseJSON = withObject "VersionRange" go where go o = do lv <- (o .:? "LaterVersion") >>= return . fmap V.laterVersion tv <- (o .:? "ThisVersion") >>= return . fmap V.thisVersion ev <- (o .:? "EarlierVersion") >>= return . fmap V.earlierVersion av <- (o .:? "AnyVersion") >>= \ (_::Maybe [(Int,Int)]) -> return $ Just V.anyVersion wv <- (o .:? "WildcardVersion") >>= return . fmap V.WildcardVersion uvr <- (o .:? "UnionVersionRanges") >>= return . fmap toUvr ivr <- (o .:? "IntersectVersionRanges") >>= return . fmap toIvr vrp <- (o .:? "VersionRangeParens") >>= return . fmap V.VersionRangeParens maybe (typeMismatch "VersionRange" $ Object o) return (lv <|> tv <|> ev <|> uvr <|> ivr <|> wv <|> vrp <|> av) toUvr [v0, v1] = V.unionVersionRanges v0 v1 toIvr [v0, v1] = V.intersectVersionRanges v0 v1

Any and all comments and suggestions are more than welcome!

Categories: Offsite Blogs

Reducing boilerplate

haskell-cafe - Sat, 03/05/2016 - 3:56pm
Hi, To write FFI bindings, I use c-storable-deriving [1] to automatically derive CStorable instances for many data types (the only difference between Storable and CStorable is that CStorable provides default methods for types that have Generic instances): {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} ... data X = X { fieldStatus :: Vector 24 Word8 , fieldPadding :: Word8 } deriving (Generic, CStorable) However I also need a Storable instance, hence I have to write (the "c*" methods are provided by CStorable): instance Storable X where peek = cPeek poke = cPoke alignment = cAlignment sizeOf = cSizeOf Is there a way to automatically generate this instance for every data that has an instance of CStorable? Ideally, I would like to say once and for all: instance CStorable a => Storable a where peek = cPeek poke = cPoke alignment = cAlignment sizeOf = cSizeOf As I don't think it is currently possible, w
Categories: Offsite Discussion

Digraphs With Text: More flexible than graphs,eager to hear from you

haskell-cafe - Sat, 03/05/2016 - 10:06am
This is a demonstration of DWT, a data structure built from and more flexible than graphs. It is powered by the *wonderful* Functional Graph Library. We beseech your involvement! DWT is open-source and actively seeking co-developers. I would happily trade any and all the privilege of determining tasks, teaching haskell or math, learning anything, and receiving obligations. We surely have much knowledge to trade! Even just a "hey why don't you do [this]!" could be precious to me. This transcript makes tiny digressions about what monads make possible. graph). (0,"0: frog") that expression. None do, because none yet exist. Such contexts offer many possibilities for tracking where you are (the data) and how you got there (also kind of the data, and perhaps enabling a desirable kind of removal of self|redaction). (0,"0: frog") (0,"1: moist") (0,"2: springy") (0,"0: frog") (0,"1: moist") (0,"2: springy") (0,":3 _ #(is a quality of) _") a : to indicate that it is a template, as opposed to the string "_ is a qual
Categories: Offsite Discussion

Accuracy of Data.Number.Fixed

haskell-cafe - Sat, 03/05/2016 - 5:50am
This does not seem right to me: Prelude Data.Number.Fixed> read "4.00" :: Fixed (EpsDiv10 (EpsDiv10 Eps1)) 4.00 Prelude Data.Number.Fixed> read "4.01" :: Fixed (EpsDiv10 (EpsDiv10 Eps1)) 4.00 Prelude Data.Number.Fixed> read "4.02" :: Fixed (EpsDiv10 (EpsDiv10 Eps1)) 4.03 Prelude Data.Number.Fixed> read "4.03" :: Fixed (EpsDiv10 (EpsDiv10 Eps1)) 4.04 Prelude Data.Number.Fixed> read "4.04" :: Fixed (EpsDiv10 (EpsDiv10 Eps1)) 4.05 Maybe I am misunderstanding the purpose of this library. I guess that "two digits" of precision means that it is accurate within +/- 0.01? I think that this library is meant for doing arbitrary-precision transcendental operations. But it would not be good as a model for something like currency. It's using ratios as an internal representation, and I'm not sure what ratios it's choosing, but I think I'd choose, say, 401/100 for the "4.01" representation. I guess it's picking a slightly smaller factor than that. The non-reversibility of read/show is somewhat disconcerting. I think I
Categories: Offsite Discussion

Call for Participation: PLACES 2016

General haskell list - Fri, 03/04/2016 - 6:50pm
--------------------------------------------------------- Call for participation: 9th Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software Friday 8th April 2016 Co-located with ETAPS 2016, Eindhoven, The Netherlands --------------------------------------------------------- For more information: http://places16.by.di.fc.ul.pt --------------------------------------------------------- Modern hardware platforms, from the very small to the very large, increasingly provide parallel computing resources for applications to maximise performance. Many applications therefore need to make effective use of tens, hundreds, and even thousands of compute nodes. Computation in such systems is thus inherently concurrent and communication centric. Effectively programming such applications is challenging; performance, correctness, and scalability are difficult to achieve. Various programming paradigms and methods have emerged to aid this task. The
Categories: Incoming News

HasCallStack - runtime costs?

haskell-cafe - Fri, 03/04/2016 - 4:53pm
Dear Cafe, the new (8.*) call stack feature https://downloads.haskell.org/~ghc/8.0.1-rc2/docs/html/users_guide/glasgow_exts.html#hascallstack is certainly nice for debugging during development. But how costly is it at runtime? I notice a 5 percent slowdown. That's not a problem if there's an easy way to switch this off for production (without changing the code). Related: how to make code that uses it, compile with older ghcs that don't have it. I made this hack: do not import GHC.Stack.Types, but instead {-# language CPP, MultiParamTypeClasses #-} #if (__GLASGOW_HASKELL__ < 710) {-# language NullaryTypeClasses #-} #endif module Stack ( HasCallStack ) where #if (__GLASGOW_HASKELL__ >= 800) import GHC.Stack.Types #else class HasCallStack instance HasCallStack #endif When I compile with 8.rc2, and change ">= 800" to ">= 900", I am getting the 5 percent speedup mentioned above. But does it really do what I hope it does (remove all runtime overhead that call stacks may have)? When I compile with 7.10.
Categories: Offsite Discussion

Month in Haskell Mode February 2016

haskell-cafe - Fri, 03/04/2016 - 4:49pm
Welcome Haskell Mode users, Haskell Mode progress report for February 2016. For previous issue see January 2015 <https://github.com/haskell/haskell-mode/wiki/Month-in-Haskell-Mode-January-2015> . Reddit discussion <https://www.reddit.com/r/haskell/comments/48wrru/month_in_haskell_mode_february_2016/> . <https://github.com/haskell/haskell-mode/wiki/Month-in-Haskell-Mode-February-2016#what-is-haskell-mode>What is Haskell Mode? Haskell Mode is an umbrella project for multiple Emacs tools for efficient Haskell development. Haskell Mode is an open source project developed by a group of volunteers constantly looking for contributions. For more information how to help see https://github.com/haskell/haskell-mode. <https://github.com/haskell/haskell-mode/wiki/Month-in-Haskell-Mode-February-2016#important-developments>Important developments Fontification received improvements so that it closer follows Haskell lexical rules. It was necessary to change to syntax-propertize-function available only starting with Emac
Categories: Offsite Discussion

Test email

libraries list - Thu, 03/03/2016 - 7:54pm
Please disregard -- sorry for the noise. Gershom
Categories: Offsite Discussion

Order of Map.fromListWith

haskell-cafe - Thu, 03/03/2016 - 7:23pm
Does anybody know why for fromListWith, the arguments to the combining function seem flipped? > import Data.Map > fromListWith (++) [('a',[1]),('a',[2])] fromList [('a',[2,1])] I often use it to group things by some key, e.g. postsByUserId :: Map Int [Int] postsByUserId = fromListWith (++) [ (userId, [postId]) | (userId, postId) <- posts ] and regularly get tricked by the postIds being reversed in the result. This is especially unintuitive to me since: > foldl (++) [] [[1],[2]] [1,2] > foldr (++) [] [[1],[2]] [1,2] Any ideas?
Categories: Offsite Discussion

Function that put elements in Left or Right side ofEither depending on type

haskell-cafe - Thu, 03/03/2016 - 5:04pm
I want a function fun :: q -> Either a b where q is of type a or b. fun shall work in the following way fun x gives Left x if x :: a fun x gives Right x if x :: b Following is a more precise description of what I want. I have function fun1 and fun2 newtype Vec k b = V [(b,k)] deriving (Eq,Ord,Show) fun1 :: (Num k) => a -> Either a (Vec k a) fun1 = Left fun2 :: (Num k) => Vec k a -> Either a (Vec k a) fun2 = Right that work in the following way {- Left 6 Right (V [(6,1)]) -} I want a overloaded function ‘fun' such that {- Left 6 Right (V[(6,1)]) -} I have tried to use a type class to do this (see code below). But when I try I get the following error Could not deduce (Num a0) from the context (Num a, Fun a b v) bound by the inferred type for ‘it’: (Num a, Fun a b v) => Either b (v b) at <interactive>:70:1-5 The type variable ‘a0’ is ambiguous When checking that ‘it’ has the inferred type it :: forall a b (v :: * ->
Categories: Offsite Discussion

apfelmus: FRP — Video of my Talk at Bobkonf 2016

Planet Haskell - Thu, 03/03/2016 - 3:17pm

Two weeks ago, I had the pleasure of attending the BOB Konferenz 2016 in Berlin, Germany, where I gave an introductory talk on functional reactive programming (FRP) in english. The talk was videotaped and the recording is now available online. So, if you like to hear a short introduction from me on what FRP is all about, and why it’s a good idea, I invite you to have a look. Slides are available, too.

The purpose of the conference was to bring together

[…] developers, architects and builders to explore technologies beyond the mainstream and to discover the best tools available today for building software.

My favorite talks were the presentation by Andres Löh on the Servant library, which allows the specification of REST APIs in the type system and eliminates a lot of boilerplate, and the talk by Stefan Wehr on the Swift language (that new language by Apple), where he demonstrated that functional programming actually has already become mainstream.

Categories: Offsite Blogs

LambdaCube: Tuples as heterogeneous lists

Planet Haskell - Thu, 03/03/2016 - 2:42pm

You probably know that lists and tuples are in no way special data types in Haskell. They are basically the following ADTs (algebraic data types) with special syntax:

data List a -- syntax in type context: [a] = Nil -- syntax in expression context: [] | Cons a (List a) -- syntax in expression context: (a : as) data Tuple2 a b -- syntax in type context: (a, b) = Tuple2 a b -- syntax in expression context: (a, b) data Tuple3 a b c -- syntax in type context: (a, b, c) = Tuple3 a b c -- syntax in expression context: (a, b, c) data Tuple4 a b c d -- syntax in type context: (a, b, c, d) = Tuple4 a b c d -- syntax in expression context: (a, b, c, d) ...

All right, but what exactly does that ... mean at the end? Do infinite tuples exist? Or at least, are there infinitely many tuples with different arities? In the case of GHC the answer is no, and this is very easy to demonstrate. Try to enter this tuple in ghci:

GHCi, version 7.10.3: http://www.haskell.org/ghc/ :? for help Prelude> (0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0) <interactive>:2:1: A 63-tuple is too large for GHC (max size is 62) Workaround: use nested tuples or define a data type

Although this seems reasonable, those who strive for perfection are not satisfied. What is the right solution for this problem? What is the real problem by the way?

I consider the Tuple2, Tuple3, Tuple4, … ADT family an inferior representation of tuples because of the following reasons:

  1. There is this ugly … at the end with several consequences.
  2. This family has no proper beginning. We can define both Tuple0 and Tuple1, but one-element tuples are not yet embraced by the Haskell community.
  3. Tuples with different arities are not related to each other, because they are defined separately, not at once as one data family. One consequence of this is that it is not possible to write generic functions for tuples.

What would be a better representation of tuples? Heterogeneous lists, of course!

data HList :: List Type -> Type where HNil :: HList 'Nil HCons :: forall t ts . t -> HList ts -> HList ('Cons t ts)

Some examples:

HNil :: HList 'Nil HCons True HNil :: HList ('Cons Bool 'Nil) HCons 3 (HCons True HNil) :: HList ('Cons Int ('Cons Bool 'Nil)

The syntactic sugar for heterogeneous lists could be the same as for tuples, for example

() ==> HNil -- in expression context () ==> HList 'Nil -- in type context (3, True) ==> HCons 3 (HCons True HNil) -- in expression context (Int, Bool) ==> HList ('Cons Int ('Cons Bool 'Nil) -- in type context

What are the issues of representing tuples by heterogeneous lists?

  1. There is a thing called one-element tuple, which needs explicit syntax.
  2. We need some type system extensions (at least GADTs and type level lists are needed).
  3. The compiler backend has to be a little bit smarter to produce efficient code for tuples.
  4. Pattern matching on tuples is not obvious anymore.

The LambaCube 3D compiler solves the above issues the following way:

  1. One element tuples are denoted by (( element )).
  2. The compiler has a dependently typed core language, therefore defining and using the HList data type works out-of-the-box.
  3. Currently the compiler has no code generator for CPUs and it has only a limited code generator for GPUs with no support for tuples. Tuples either vanish during reduction, or they are transformed away in the shader code generator.
  4. Pattern matching on heterogeneous lists is restricted: when a tuple is matched, all patterns should have the same tuple arity. We’re okay with this, since this behaviour is not surprising for most programmers, and in LambdaCube 3D code tuple patterns tend to appear without alternative choices anyway.

After solving these issues, and migrating to the new representation of tuples, the built-in LambdaCube 3D library could be simplified significantly.

Some examples: previously we had repetitive, incomplete and potentially wrong functions for tuples like

type family JoinTupleType t1 t2 where JoinTupleType a () = a JoinTupleType a (b, c) = (a, b, c) JoinTupleType a (b, c, d) = (a, b, c, d) JoinTupleType a (b, c, d, e) = (a, b, c, d, e) JoinTupleType a b = (a, b) -- this is wrong if b is a 5-tuple! -- JoinTupleType a ((b)) = (a, b) -- something like this would be OK remSemantics :: ImageSemantics -> Type remSemantics = ... -- definition is not relevant now remSemantics_ :: [ImageSemantics] -> Type remSemantics_ [] = '() remSemantics_ [a] = remSemantics a -- not good enough... -- remSemantics_ [a] = '((remSemantics a)) -- something like this would be OK remSemantics_ [a, b] = '(remSemantics a, remSemantics b) remSemantics_ [a, b, c] = '(remSemantics a, remSemantics b, remSemantics c) remSemantics_ [a, b, c, d] = '(remSemantics a, remSemantics b, remSemantics c, remSemantics d) remSemantics_ [a, b, c, d, e] = '(remSemantics a, remSemantics b, remSemantics c, remSemantics d, remSemantics e)

With heterogeneous lists as tuples these and similar functions shrank considerably:

type family JoinTupleType a b where JoinTupleType x (HList xs) = HList '(x: xs) remSemantics_ :: [ImageSemantics] -> Type remSemantics_ ts = 'HList (map remSemantics ts)

By the way, with heterogeneous lists it was also easier to add row polymorphism (one solution for generic records) to the type system, but that is a different story.

The pattern matching issue deserves a bit more detail. Why is it a good idea to restrict pattern matching for heterogeneous lists? Well, consider the following function with no type annotation:

swap (a, b) = (b, a)

Of course we expect the compiler to infer the type of swap. On the other hand, if tuples are heterogeneous lists, the following function is also typeable:

f (_, _) = 2 f (_, _, _) = 3 f _ = 0

It seems that type inference is not feasible for heterogeneous lists in general. For LambdaCube 3D we settled with above mentioned restriction in order to retain type inference. It seems feasible to create a system that allows the definition of f with a type annotation, but this would not buy much for the users of LambdaCube 3D so we didn’t go for it.

I have found a few implementations of heterogeneous lists in Haskell, Idris and Agda. So far I have not found a language where tuples are represented with heterogeneous lists, neither a language with special syntax for heterogeneous lists.

  1. HVect in reroute package is the same as HList.
  2. HVect in hvect package is a strict variant of HList.
  3. Tuples in Idris are different: (x, y, z) is a synonym for (x, (y, z)). On the other hand, HVect in the standard library is similar to HList. The difference is that the type level list is indexed by its length. I have found this discussion about whether tuples could be represented with HVect. It seems that efficient code generation is the difficult part.
  4. I have found an implementation of HList and HVec in Agda. However, I also found this discussion about size problems, so it is not so convenient to use them. We don’t have such issues because we use type-in-type.
  5. https://wiki.haskell.org/Heterogenous_collections gives a summary about implementing heterogeneous collections in Haskell. Heterogeneous lists are at the bottom (see next item).
  6. Strongly typed heterogeneous collections by Oleg Kiselyov has a more complicated implementation of heterogeneous lists in Haskell using less type system extensions.

To sum it up, in the case of LambdaCube 3D, representing tuples as heterogeneous lists has no drawback and at the same time the base library (which provides the OpenGL binding) became more complete, shorter and more correct. We definitely consider switching to this representation an overall win.

Categories: Offsite Blogs