Fun with Type Functions[edit]

Here is Version 3 of our paper (May 2010):

Fun With Type Functions (version 3), Oleg Kiselyov, Ken Shan, and Simon Peyton Jones. This online version includes an Appendix that does not appear in the printed version.
Slides (PDF)
Source code

which will appear in the proceedings of Tony Hoare's 75th birthday celebration.

Abstract. Tony Hoare has always been a leader in writing down and proving properties of programs. To prove properties of programs automatically, the most widely used technology today is by far the ubiquitous type checker. Alas, static type systems inevitably exclude some good programs and allow some bad ones. This dilemma motivates us to describe some fun we've been having with Haskell, by making the type system more expressive without losing the benefits of automatic proof and compact expression.

Haskell's type system extends Hindley-Milner with two distinctive features: polymorphism over type constructors and overloading using type classes. These features have been integral to Haskell since its beginning, and they are widely used and appreciated. More recently, Haskell has been enriched with type families, or associated types, which allows functions on types to be expressed as straightforwardly as functions on values. This facility makes it easier for programmers to effectively extend the compiler by writing functional programs that execute during type-checking.

This paper gives a programmer's tour of type families as they are supported in GHC today.

This Wiki page is a discussion page for the paper. If you are kind enough to read this paper, please help us by jotting down any thoughts it triggers off. Things to think about:

What is unclear?
What is omitted that you'd like to see?
Do you have any cool examples that are of a somewhat different character than the ones we describe? (If so, do explain the example on this page!)

You can identify your entries by preceding them with four tildes. Doing so adds your name, and the date. Thus:

Simonpj 08:42, 19 April 2007 (UTC) Note from Simon

If you say who you are in this way, we'll be able to acknowledge your help in a revised version of the paper.

Add comments here (newest at the top):

JeanPhilippeBernardy 10:01, 22 August 2010 (UTC) In the 3rd paragraph: Every type system excludes some “good” programs, and permits some “bad” ones.

I believe this should say "or", not "and".

ChrisKuklewicz 06:58, 21 August 2010 (UTC) The paper still mentions 6.10 as the newest GHC instead of 6.12: "However, such equality superclasses are not yet implemented in the latest release of GHC (6.10)."

Version 2[edit]

Stuff below here refers to Version 2 of the paper, now retired. I believe I have responded to all the suggestions below: thank you very much! SLPJ

Norman Ramsey 16:51, 3 March 2010 (UTC) When the distinction between {{{data}}} and {{{type}}} is introduced in section 2.4, I'd like to be reassured that the compiler guarantees injectivity, and to get a brief explanation of the mechanism (I think it's the uniqueness of the value constructor, but I'm not 100% confident).

Norman Ramsey 1 March 2010: I'd really like to see an alert before the example that introduces 'data' in a class declaration. The difference had me totally distracted from the rest of the example.

tanimoto 03:38, 20 July 2009 (UTC) Comments not aligned correctly

In Appendix A, item 1, "ILLEGAL" and "OK" could be aligned with the previous comments.

In Appendix A, item 3, type T5, "OK" is not aligned with the previous comments. The same goes for the signature.

Some code snippets go off the right margin, I hope it's not a problem: pp. 10, 17, 18, 25, 35, 37.

bens 01:13, 20 July 2009 (UTC) In Appendix C, "fmt1 ^ fmt2 = fmt1 ++ \x -> fmt2 x" -> "fmt1 ^ fmt2 = \x -> fmt1 ++ fmt2 x".

BobAtkey 17:39, 9 July 2009 (UTC) Could you update the reference to my "Parameterised Notions of Computation" paper to the journal version? Thanks: Robert Atkey. Parameterised Notions of Computation. Journal of Functional Programming 19: (3 & 4), pages 355-376, July 2009.

Mvanier 03:14, 3 July 2009 (UTC) The source code link seems to be dead. SLPJ: fixed

Version 1[edit]

Stuff below here refers to Version 1 of the paper, now retired.

Oleg 02:55, 3 June 2009 (UTC)

Thank you indeed for all the comments and suggestions!

i have dealt with all the comments and fixed all the noted problems. I have a few questions about several suggestions though. I should remark first that the complete code discussed in the paper is available, presently in our darcs repository. I guess Simon has not decided of a site to host the online version of the paper with the Appendices and the code. Incidentally, code fragments in the paper are lifted straight from the working code, using the remarkably useful \VerbatimInput.

Byorgey 20:07, 19 May 2009 (UTC)

p. 32:
- "powerful, but the" -> "powerful, but they"
p. 33:
- "commonly mentioned on Haskell mailing lists pitfall of type functions" -> "one pitfall of type functions commonly mentioned..."
- "the compiler should chose" -> "should the compiler choose"

BerniePope 06:18, Fri 15 May 2009 (UTC) Typo in Appendix B.

"GHC should noat" -> "GHC should not"

tanimoto 02:17, 15 May 2009 (UTC) Typo in references

In reference [32], page 30, Oleg's last name is misspelled as "Kiselov".

Ryani 23:01, 14 May 2009 (UTC) Fun paper! Comments:

I was writing a generic finite map a while ago and determined that the generic memoized trie was better in almost all cases; it was simpler semantically and didn't have a significant performance difference. Then you have "type Map k v = Table k (Maybe v)". Is it worth calling out this special case in its own section?

Also, in respose to ChrisKuklewicz, I think the type for "cons" is correct, but perhaps one instance should be given as an example.

To Ryan Ingram: Just to double-check: you are saying that the implementation of generic finite maps as "type Map k v = Table k (Maybe v)" is faster that the one given in Sec 3.3? That is quite interesting!

Dave Menendez 16:52, 14 May 2009 (UTC) On page 11, you refer to a "specialised instance for Table Int that uses some custom (but innite!) tree representation for Int." Was this meant to be Integer? Surely any tree representation for Int would be large but finite.

Peter Verswyvelen and I have been working on some type family fun to give us generalised partial application (even to the point of being able to cope with giving arguments, but not a function). I don't know if it really makes any interesting point that you didn't already in the paper, but it's certainly fun...

{-# LANGUAGE TypeFamilies, EmptyDataDecls, TypeOperators, FlexibleInstances, FlexibleContexts #-}

module Burn2 where

newtype V a = V a -- A value
data    B a = B   -- A value we don't want to provide yet

-- Type level homogenous lists (well just tuples in a list-like syntax really)
data Nil a = Nil
data a :& b = !a :& !b

infixr 5 :& 

class Apply funargs where
  type Result funargs :: *
  apply :: funargs -> Result funargs

instance (Apply (V b :& rest), a ~ c) => Apply (V (a->b) :& V c :& rest) where
  type Result  (V (a->b) :& V c :& rest) = Result (V b :& rest)
  apply (V f :& V a :& rest) = apply $ V (f a) :& rest

instance (Apply (V b :& rest), a ~ c) => Apply (B (a->b) :& V c :& rest) where
  type Result (B (a->b) :& V c :& rest) = (a->b) -> Result (V b :& rest)
  apply (B :& V a :& rest) = \f -> apply $ V (f a) :& rest

instance (Apply (V b :& rest), a ~ c) => Apply (V (a->b) :& B c :& rest) where
  type Result  (V (a->b) :& B c :& rest) = a -> Result (V b :& rest)
  apply (V f :& B :& rest) = \a -> apply $ V (f a) :& rest

instance (Apply (V b :& rest), a ~ c) => Apply (B (a->b) :& B c :& rest) where
  type Result (B (a->b) :& B c :& rest) = (a->b) -> a -> Result (V b :& rest)
  apply (B :& B :& rest) = \f a -> apply $ V (f a) :& rest

instance Apply (V a :& Nil b) where
  type Result  (V a :& Nil b) = a
  apply (V a :& Nil) = a

instance Apply (B a :& Nil b) where
  type Result  (B a :& Nil b) = B a
  apply (B :& Nil) = B

v1 = apply (V 1 :& Nil)
f1 = apply (B :& Nil)
v2 = apply (V negate :& V 1 :& Nil)
f3 = apply (V negate :& B :& Nil)
v3 = apply (V f3 :& V 1 :& Nil)

Beelsebob 13:04, 14 May 2009 (UTC)

To Beelsebob: I'm afraid the code does not account for the most interesting case: a function that takes a dynamic value and returns a static result. So you need to deal with functions of the type V a -> B b or B a -> V b. The literature on partial evaluation describes this issue in detail. Our tagless-final paper (Sec 4.2 of the the journal version, Delaying binding-time analysis) has a short explanation, too.

End of section 2.2, I think "cons :: a -> [b] -> [ResTy a b]" should be "cons :: a -> [b] -> ResTy a b"

ChrisKuklewicz 15:28, 14 May 2009 (UTC)

End of page 19 with footnote 9. I could not simply copy and paste the URL because of a stray space after the '-' in http://okmij.org/ftp/Haskell/keyword- arguments.lhs

ChrisKuklewicz 16:08, 14 May 2009 (UTC)

To Chris Kuklewicz, regarding the problem with footnote 9. That is an odd problem that I could not reproduce. It seems xpdf lets me cut and paste the URL in question without introducing stray spaces. BTW, the type was correct, as Ryan Ingram described. We have implemented his suggestion so to remove the confusion.

Typo "Mounier" --> "Monnier"

Tom Schrijvers 11:11, 15 May 2009 (UTC)

Contrary to what the introductions say, polymorphism over type constructors was not part of Haskell from the beginning. They were only introduced after Mark Jones showed how to do it in Gofer.

Augustss 14:30, 15 May 2009 (UTC)

Why do you say "Obviously, we want to declare algebraic data kinds, ..."? What's obvious about that? Many of us think that's the wrong way, and you should instead provide a way to lift ordinary data type to the kind level.

Augustss 15:36, 15 May 2009 (UTC)

I was really fascinated by section 5.2 where you track state in the types using a parameterized monad. However, the example code you use is rather underwhelming since it can be implemented by much simpler means. If there's only a fixed number of locks then they can be tracked using a fixed tuple and the whole type functions business is a bit superfluous (albeit still nice). To really reap the benefits of the machinery you set up you ought to have a function for creating new locks dynamically. Here's an example of how it can be done:

type family Length p
type instance Length Nil = Zero
type instance Length (Cons l p) = Succ (Length p)

type family NewLock p
type instance NewLock Nil = Cons Unlocked Nil
type instance NewLock (Cons l p) = Cons l (NewLock p)

newLock :: Nat (Length p) =>
           LockM p (NewLock p) (Lock (Length p))
newLock = LockM (return mkLock)

In order for this to work nicely we need a new run function as well. I've used an ordinary type class to check that all locks are unlocked, since this really is a predicate on the state and not a function.

class AllUnlocked a

instance AllUnlocked Nil
instance AllUnlocked p => AllUnlocked (Cons Unlocked p)

runNew :: AllUnlocked locks => LockM Nil locks a -> IO a
runNew = unLockM

I think the section becomes more convincing if you add dynamic creation of locks. Not to mention the increased sex appeal :-)

Josef 16:58, 25 May 2009 (UTC)

To Josef Svenningsson: indeed the variable number of locks would have been sexier but it creates the problem of locks `leaking' out of scope (e.g., returned as the result of runNew and then used within another runNew computation, with disastrous results). In short, we need regions. Chung-chieh Shan and I have indeed implemented such a system, with a parameterized monad to track the state of the variable number of resources (file handles in our case). Please see Sec 6 of our Lightweight Monadic Regions paper. We used functional dependencies for type functions. Replacing functional dependencies with type functions is straightforward. Yet the staggering complexity of the code in Sec 6 will remain. I'm afraid this makes the example too complex for this paper; rather than attracting users to type functions we would scare all of them away.

It would be very nice if you published a bundle or repository somewhere containing the Haskell source from the paper. At the very least it would be nice with a comment on which version of GHC one should have and what flags are required. The reason I'm asking is that I had a bit of trouble with this. For instance, just saying {-# LANGUAGE TypeFamilies #-} didn't enable type equality constraints in the parser. I had to add ScopedTypeVariables which felt rather arbitrary.

Josef 16:58, 25 May 2009 (UTC)