# Simonpj/Talk:FunWithTypeFuns

### From HaskellWiki

Line 54: | Line 54: | ||

module Burn2 where | module Burn2 where | ||

− | newtype V a = V a -- A value | + | newtype V a = V a -- A value |

data B a = B -- A value we don't want to provide yet | 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) | + | -- Type level homogenous lists (well just tuples in a list-like syntax really) |

− | data Nil a = Nil | + | data Nil a = Nil |

data a :& b = !a :& !b | data a :& b = !a :& !b | ||

infixr 5 :& | infixr 5 :& | ||

− | class Apply funargs where | + | class Apply funargs where |

− | type Result funargs :: * | + | type Result funargs :: * |

apply :: funargs -> Result funargs | apply :: funargs -> Result funargs | ||

− | instance (Apply (V b :& rest), a ~ c) => Apply (V (a->b) :& V c :& rest) where | + | 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) | + | type Result (V (a->b) :& V c :& rest) = Result (V b :& rest) |

apply (V f :& V a :& rest) = apply $ V (f a) :& 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 | + | 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) | + | 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 | 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 | + | 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) | + | type Result (V (a->b) :& B c :& rest) = a -> Result (V b :& rest) |

apply (V f :& B :& rest) = \a -> apply $ V (f a) :& 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 | + | 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) | + | 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 | apply (B :& B :& rest) = \f a -> apply $ V (f a) :& rest | ||

− | instance Apply (V a :& Nil b) where | + | instance Apply (V a :& Nil b) where |

− | type Result (V a :& Nil b) = a | + | type Result (V a :& Nil b) = a |

apply (V a :& Nil) = a | apply (V a :& Nil) = a | ||

− | instance Apply (B a :& Nil b) where | + | instance Apply (B a :& Nil b) where |

− | type Result (B a :& Nil b) = B a | + | type Result (B a :& Nil b) = B a |

apply (B :& Nil) = B | apply (B :& Nil) = B | ||

## Revision as of 18:31, 14 May 2009

# Fun with Type Functions

Oleg Kiselyov, Ken Shan, and Simon Peyton Jones have a draft paper

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, orassociated 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!)

Deadline is sometime in June 2009.

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):

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 inﬁnite!) 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)

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)