June 2009 - Haskell-Cafe

Re: [Haskell-cafe] Building a tree?
by michael rice 12 Jun '09

12 Jun '09

Example understood. Thanks. Is there a module for binary trees? Michael --- On Wed, 6/10/09, wren ng thornton <wren(a)freegeek.org> wrote: From: wren ng thornton <wren(a)freegeek.org> Subject: Re: [Haskell-cafe] Building a tree? To: haskell-cafe(a)haskell.org Date: Wednesday, June 10, 2009, 8:13 PM michael rice wrote: > Here's a function from Data.Tree: > > unfoldTree :: (b -> (a, [b])) -> b -> Tree a > Build a tree from a seed value > > Could someone please give me a brief example of usage. Data.Tree> let t = unfoldTree (\i -> (show i, [i`div`2..i-1])) Data.Tree> putStr . drawTree $ t 8 -- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe(a)haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

6 5

List comprehensions and impredicative rank-N types
by Vladimir Reshetnikov 11 Jun '09

11 Jun '09

Hi, Consider the following definitions: ----------------------------------------------------------- {-# LANGUAGE RankNTypes, ImpredicativeTypes #-} foo :: [forall a. [a] -> [a]] foo = [reverse] bar :: [a -> b] -> a -> b bar fs = head fs ----------------------------------------------------------- According to the Haskell Report, [f | f <- foo] translates to (let ok f = [f]; ok _ = [] in concatMap ok foo), right? So, I wonder why (bar [f | f <- foo]) typechecks, but (bar (let ok f = [f]; ok _ = [] in concatMap ok foo)) and (bar foo) do not typecheck? Thanks, Vladimir

1 0

who's up for a hackathon? (ICFP, late Aug, early Sept)
by Eric Kow 11 Jun '09

11 Jun '09

Dear Haskellers, ICFP 2009 takes place from Monday 31 August to Wednesday 2 September, with the Haskell Symposium following it on 3 September. Would anybody be interested having a Haskell Hackathon during this? My thinking is that to catch people who are only going to the Haskell Symposium, the best time is the following weekend (4-6 September). Otherwise, the weekend before (29-30 August) is also an option and has the benefit of catching people before they get tired :-) Rah, rah, hackathon! 1. If possible, I'd like get a idea if there is any interest in attending such a Hackathon if it were to take place. 2. For rah-rah Hackathon to work, we need people! Could I get one kind (and local) soul to act as an organiser for this? Thanks! -- Eric Kow <http://www.nltg.brighton.ac.uk/home/Eric.Kow> PGP Key ID: 08AC04F9

2 1

a cool paper (.pdf) on Cabal?
by Vasili I. Galchin 11 Jun '09

11 Jun '09

Hello, Before I found a really cool paper on Cabal motivation and architecture. I can no longer find this paper. Any ideas/suggestions? Kind regards, Vasili

3 3

Re: [Haskell] ANNOUNCE: testrunner-0.9
by Max Bolingbroke 11 Jun '09

11 Jun '09

2009/6/8 Reinier Lamers <tux_rocker(a)reinier.de>: > I checked out testpack and that did not meet my requirements. I don't know if > I considered test-framework. If I did, it may be that I was turned off by the > fact that the 'home page' link on cabal just goes to a web presentation of the > source tree on github. Reinier, You are quite right that this is a weakness. I've been meaning to put a site together for a while, and your comment gave me the impetus to do it: http://batterseapower.github.com/test-framework/ That's much friendlier! All the best, Max

3 3

ANNOUNCE: Galois is hiring functional programmers
by Don Stewart 11 Jun '09

11 Jun '09

Galois is hiring. Bringing together mathematicians, researchers and technologists, Galois, based in Portland, Oregon, was founded in 1999 with the mission to apply functional languages and formal methods to solve real world problems. Today, over 30 members strong, we’re living the vision, designing and developing advanced technologies for safety and security-critical systems, networks, and applications. Galois technical staff members play a pivotal role in developing advanced software technology. Members work on one or more projects, and are expected to perform in a variety of roles based upon their talents and organizational needs. Technical staff may be called upon to write proposals, gather requirements, and work in all stages of the software development process, from requirements gathering to testing and validation. Additional duties may include project management, technology research and development, and technical infrastructure development. We’re looking for people who can invent, learn, think, and inspire. We reward creativity and thrive on collaboration. We offer great benefits and perks, including a 401K plan, stock options, paid vacation, family health plan, flexible work schedule, a casual work environment, snacks, espresso and foosball. Galois technical staff members usually work in a small team setting (2-5 members), and must successfully interact with clients, partners, and other employees in a highly cooperative, collaborative, and intellectually challenging environment. A Masters or Ph.D. degree in Computer Science is desirable but not required. Additionally, a strong programming background and experience with Haskell or other functional programming languages is preferred but not required. Must work well with customers, including building rapport, identifying needs, and communicating with strong written, verbal and presentation skills. Must be highly motivated and able to self-manage to deadlines and quality goals. To learn more about us, visit http://www.galois.com and http://www.galois.com/company/careers The types of technology we use are covered in our blog: http://www.galois.com/blog/ We’d like to hear from you! Send your cover letter and resume to us at jobs2009(a)galois.com.

1 0

Lightweight type-level dependent programming in Haskell
by Ryan Ingram 11 Jun '09

11 Jun '09

(Literate Haskell post) > {-# LANGUAGE GADTs, RankNTypes, TypeFamilies, ScopedTypeVariables, FlexibleContexts #-} > module Dependent where I recently discovered an interesting way of closing typeclasses while playing with type-level peano naturals: First we build peano integers at the type level: > data Z = Z > newtype S n = S n And a couple of generally useful type-level combinators: > newtype I x = I { unI :: x } > newtype K x y = K { unK :: x } (We could also include the S combinator, under a different name, but I haven't needed it yet...) This representation isn't "closed"; there's nothing forcing the "n" in S n to be Z or S n. But we can make a typeclass easily: class Nat n instance Nat Z where ... instance Nat n => Nat (S n) where ... But again, this typeclass is open. What I recently realized is that it's easy to close the typeclass by requiring instances to provide a simple implementation of "typecase": > class Nat n where > caseNat :: forall r. n -> (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> r By parametricity, any non _|_ implementation of caseNat has to prove either (n ~ Z), to call the first branch, or (n ~ S p) for some other natural p, to call the second. > instance Nat Z where > caseNat _ z _ = z > instance Nat n => Nat (S n) where > caseNat (S n) _ s = s n (Interesting side note: the S n pattern match is automatically lazy, since S is a newtype) Somewhat surprisingly, caseNat is sufficient to prove *dependent* induction: > induction :: forall p n. Nat n => n -> p Z -> (forall x. Nat x => p x -> p (S x)) -> p n > induction n z s = caseNat n isZ isS where > isZ :: n ~ Z => p n > isZ = z > isS :: forall x. (n ~ S x, Nat x) => x -> p n > isS x = s (induction x z s) What does this function mean? Through the Curry-Howard lens, it says: If we have a proof of P 0, and a proof of (P x -> P (x+1)) for any natural x, then we can prove P n for any natural n! The proof simply proceeds by case analysis on n; we know that the proof terminates since the recursive step works at a strictly smaller type, and Haskell types are all finite in size. Now, of course, this isn't any different from case analysis on this GADT: > data Peano a where > Pz :: Peano Z > Ps :: Peano n -> Peano (S n) > inductP :: forall n p. Peano n -> p Z -> (forall x. Peano x -> p x -> p (S x)) -> p n > inductP Pz z s = z > inductP (Ps n) z s = s n (inductP n z s) In fact, the whole point of GADT case analysis is to introduce the type-level coercions that caseNat makes explicit. So there's not a huge gain here. There is one interesting benefit that the typeclass answer gives you, however; you can let the compiler derive the proof for you: > witnessNat :: forall n. Nat n => n > witnessNat = theWitness where > theWitness = unI $ induction (undefined `asTypeOf` theWitness) (I Z) (I . S . unI) Then we can optimize the implementation of witness to "unsafeCoerce Z" after the typechecker agrees with our proof. Another useful tool is existentials and witnesses; existentials allow you to do value-level calculation on "Nat"; witnesses allow you to construct a proof of Nat n and return it from a proof; there's no other way to return that something is a member of a typeclass. > data AnyNat where AnyNat :: Nat n => n -> AnyNat > data IsNat n where IsNat :: Nat n => IsNat n > mkNat :: Integer -> AnyNat > mkNat x | x < 0 = error "Nat must be >= 0" > mkNat 0 = AnyNat Z > mkNat x = case (mkNat (x-1)) of (AnyNat n) -> AnyNat (S n) > natToInteger :: Nat n => n -> Integer > natToInteger n = unK $ induction n (K 0) (K . (+1) . unK) > prec_app = 11 > instance Show AnyNat where > showsPrec p (AnyNat n) = showParen (p > prec_app) (showString "mkNat " . shows (natToInteger n)) Fun exercises: > data TEq a b where TEq :: (a ~ b) => TEq a b 1) Write a sized list GADT, and build some lists using combinators on Nat. Here's an example: myReplicate a = induction witnessNat Nil (Cons a) For me, ghc correctly infers this function to have the type myReplicate :: (Nat n) => a -> List a n. It's nice that I don't have to specify n anywhere! Try implementing fold :: Nat n => (forall x. Nat x => a -> p x -> p (S x)) -> List a n -> p n 2) (Easy) Prove that all sized lists have a length that is a natural number: lengthIsNat :: SizedList a n -> IsNat n 3) Prove that equality is decidable on naturals: natEqDec :: forall x y. (Nat x, Nat y) => x -> y -> Maybe (TEq x y) 4) Write the standard "plus" type family, then prove: plusIsNat :: forall x y. (Nat x, Nat y) => IsNat (Plus x y) plusIsComm :: forall x y. (Nat x, Nat y) => TEq (Plus x y) (Plus y x) (While doing this exercise, I was impressed at how good the type coercion prover is) 5) (Challenge) Write definitions for "instance Eq AnyNat" and "instance Num AnyNat"

3 2

Re: FlexibleContexts and FlexibleInstances
by Niklas Broberg 11 Jun '09

11 Jun '09

Hi Claus, What you describe is exactly how I would *want* things to work. It's nice to hear my wishes echoed from a user perspective. :-) On Wed, Jun 10, 2009 at 4:43 PM, Claus Reinke<claus.reinke(a)talk21.com> wrote: > just a few comments from a user (who would really, really, like to be > able to define pragma collections, so that he doesn't have to switch > on half a dozen separate extensions every time;-). > >> The following toy program requires MultiParamTypeClasses OR >> FlexibleContexts in order to be accepted by GHC(i): >> >>> f :: (T a b) => a -> Int >>> f _ = 0 >> >> This of course assumes that we import the definition of T, we *must* >> have MultiParamTypeClasses enabled if we want to declare T. Both >> extensions thus enable classes with more than one argument to appear >> in contexts. > > Only MultiParamTypeClasses does (and neither extension is needed in the > module defining 'f', if 'T' is imported, which suggests that > MultiParamTypeClasses is propagated to importers - this isn't true for > most other extensions). The documentation still points to -fglasgow-exts, so > it doesn't seem to answer these questions.. Right you are - which seems very strange to me. GHC accepts the module defining 'f' with no flags at all, even though it is clearly not Haskell 98. I'd go so far as to say that's a bug (as opposed to just unwanted/unexpected behavior). >>> f :: (T a ()) => a -> Int >>> f _ = 0 >> >> i.e. changing the second argument to T to () instead, means we now >> *must* have FlexibleInstances, in order to allow the non-tyvar >> argument. This is nothing surprising, this is what FlexibleInstances >> are supposed to do. > > You mean FlexibleContexts. Indeed I do. >> Now, FlexibleInstances *also* lifts the restriction on contexts, just >> like FlexibleContexts - but *only* for the contexts of instance >> declarations. > > No. FlexibleInstances is about instance *heads*, FlexibleContexts is about > contexts everywhere (in practice, there are some bugs;-). Right, this is exactly what I *want* should happen, both as a user and as an implementor, but that's not how GHC does it. FlexibleInstances do enable FlexibleContexts for contexts in instance declarations - which I think is a wart. > class T a b -- requires MultiParamTypeClasses instance T a a -- requires > FlexibleInstances instance Eq () => T a [b] -- requires FlexibleContexts > instance Eq [a] => T a b -- requires UndecidableInstances Agreed - but here you avoid the tricky cases like my 'f' above. ;-) What I would want, and what I believe you want as well, is the following: ======================================== ** MultiParamTypeClasses: Enables more than one parameter in class declarations, instance heads and more than one argument to class assertions in contexts everywhere. Formally, it would mean the following changes to the Haskell 98 syntax: topdecl -> class [scontext =>] tycls tyvar1 ... tyvarn [where cdecls] (n >=1) | instance [scontext =>] qtycls inst1 ... instn [where idecls] (n >=1) context -> class | ( class1 , ... , classn ) (n>=0) class -> qtycls cls1 ... clsn (n>=1) cls -> tyvar | ( tyvar atype1 ... atypen ) (n>=1) scontext -> simpleclass | ( simpleclass1 , ... , simpleclassn ) (n>=0) simpleclass -> qtycls scls1 ... sclsn (n>=1) scls -> tyvar ** FlexibleContexts: Enables the use of non-tyvar (or tyvar applied to types) arguments to class assertions in contexts everywhere (orthogonal to whether there can be several arguments or just one). Formally it means the following syntactic changes to Haskell 98: fcontext -> fclass | ( fclass1 , ... , fclassn ) (n>=0) fclass -> qtycls atype1 ... atypen (n>=1) topdecl -> data [fcontext =>] simpletype = constrs [deriving] | newtype [fcontext =>] simpletype = newconstr [deriving] | class [fcontext =>] tycls tyvar [where cdecls] | instance [fcontext =>] qtycls inst [where idecls] gendecl -> vars :: [fcontext =>] type for the single-argument case. (Note that I wrote type in my proposal in the OP, but it should of course be atype.) ** FlexibleInstances: Enables the use of arguments other than type constructors (possibly applied to tyvars) in instances *heads* (orthogonal to whether there can be one or more arguments, and what the context may look like). Formally it means the following syntactic changes to Haskell 98: topdecl -> instance [scontext =>] qtycls inst [where idecls] inst -> atype for the single-parameter standard-context case. (Note again that it should be atype and not type as I wrote in the OP.) ======================================== This of course only touches the syntactic part. It doesn't attempt to track things like 'instance (T a a) => R a b' that would be enabled by FlexibleContexts, nor does it attempt to track things like the Paterson conditions, but the syntax is all I'm interested in at the moment. This is the stance I will use for haskell-src-exts, unless someone protests wildly. If there is any interest, I can also propose these cases as bug reports to GHC. I hesitate to make formal proposals (e.g. for Haskell') regarding these extensions since I'm not sure I have the full story regarding the non-syntactic parts. But if there is a particular interest in that then I might go the extra mile there too. Cheers, /Niklas

1 0

Building a tree?
by michael rice 11 Jun '09

11 Jun '09

Here's a function from Data.Tree: unfoldTree :: (b -> (a, [b])) -> b -> Tree a Build a tree from a seed value Could someone please give me a brief example of usage. Michael

3 3

Hac phi accommodation: register by June 15 for reduced rate!
by Brent Yorgey 10 Jun '09

10 Jun '09

Hi all, This is a quick reminder for people interested in attending Hac phi who have not yet reserved a hotel room: if you'd like to reserve a room at Club Quarters at the reduced rate ($114/night single, $129/night double), we ask that you send a note to Daniel Wagner (daniel(a)wagner-home.com) by this Monday, June 15th. To register, or for more infomation about Hac phi, visit the wiki page [1]. Thanks, and we look forward to seeing you at the hackathon! The Hac phi Team [1] http://haskell.org/haskellwiki/Hac_%CF%86

1 0