Home

Data Types a la Carte

Data Types a la Carte. Wouter Swierstra.

This paper describes a technique for assembling both data types and functions from isolated individual components. We also explore how the same technology can be used to combine free monads and, as a result, structure Haskell’s monolithic IO monad.

This new Functional Pearl has been mentioned twice in comments (1, 2), and has now also appeared with comments on Phil Wadler's blog. Obviously it's time to put it on the front page.

By Matt Hellige at 2008-02-28 17:12 | Functional | other blogs | 24222 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Fixed Point?

The pearl centers around a definition:

data Expr f = In (f (Expr f))

I don't know much about fixed points but it looks like f is a type constructor (of kind (* -> *)). I did this in GHCi:

*Main> :type (Val 9)
(Val 9) :: Val e

I guess the e is free. Now,

*Main> :type (In (Val 9))
(In (Val 9)) :: Expr Val

What I don't understand is, how does (Val 9) of type (Val e), meaning forall e. Val e, conform to the type Val (Expr Val) as expected from the type of Expr Val? Is e getting set to Expr Val?
Is it some kind of a recursive type that has as its fixed point the type Val? But Val is not exactly a type (of kind *)! Can someone explain this wizardry in some greater details?

By uchchwhash at Fri, 2008-02-29 22:07 | login or register to post comments

Sort of...

What I don't understand is, how does (Val 9) of type (Val e), meaning forall e. Val e, conform to the type Val (Expr Val) as expected from the type of Expr Val? Is e getting set to Expr Val?

Yes.

Is it some kind of a recursive type that has as its fixed point the type Val?

Almost. Expr Val is the fixed point of Val. Expr is the fixed point operator (think Y or Mu), but we are required to roll/unroll it explicitly (using In). Expr takes a type constructor (of kind * -> *) and produces its fixed point (of kind *). In other words, we expect to have Expr Val = Val (Expr Val), and in fact, we do:

*Main> :type (Val 9) :: Val (Expr Val)
(Val 9) :: Val (Expr Val) :: Val (Expr Val)

*Main> :type In (Val 9)
In (Val 9) :: Expr Val

The two types are isomorphic under application and removal of the In constructor.

By Matt Hellige at Sat, 2008-03-01 00:24 | login or register to post comments

Thanks.

Thanks Matt for your explanation. Is that Haskell98, by the way? The article mentions that the typeclass for injection :<: is not.

By uchchwhash at Sat, 2008-03-01 02:06 | login or register to post comments

I think so

I'm not an expert, but I'm almost positive these two types are Haskell 98. In any case they work for me in ghci without -fglasgow-exts or any other mumbo-jumbo.

By Matt Hellige at Sat, 2008-03-01 18:47 | login or register to post comments

More RT and CS

There has been lots of discussion lately about the relationship between referential transparency and capability security (I'm looking at you, naasking!). In particular, we discussed the possibility of getting CS in Haskell by modularizing the IO monad. No on has mentioned it yet, but Section 7 of this pearl addresses exactly this topic, using the techniques shown just prior. It's still not as granular as true CS would demand, but it demonstrates a number of interesting points. Most interestingly, it shows that it is possible to achieve this today in Haskell, delegating fine-grained parts of IO's authority to other functions in a modular fashion. Even if you skip the rest of this paper (but why would you?) I highly recommend reading Section 7 in the light of the capabilities discussion.

It's nice how this paper just happens to bring together many recent threads on LtU. Athough I'm sad that no one has so far noted Swierstra's excellent choice of example integers...

By Matt Hellige at Tue, 2008-03-11 20:37 | login or register to post comments

Athough I'm sad that no one

Athough I'm sad that no one has so far noted Swierstra's excellent choice of example integers...

Good catch!

By Ehud Lamm at Tue, 2008-03-11 22:53 | login or register to post comments

I agree! This paper does

I agree! This paper does modularize monads somewhat, and the more fine-grained effects are welcome. The approach still seems quite complicated though, and I don't quite grok typeclass syntax very well (particularly multi-parameter typeclasses and functional dependencies). I'm more an ML modules kind of guy, particularly since typeclasses can be viewed as sugar over modules. I wonder what the formulation in terms of modules would be like.

By naasking at Wed, 2008-03-12 23:21 | login or register to post comments