Where are higher-rank and existential types used?
Hello, Norman Ramsey and I are looking for examples of where higher-rank polymorphism and existential types are useful. Can anyone think of uses besides the following? Higher-rank types are used in: - Deforestation Andrew Gill, John Launchbury, and Simon L. Peyton Jones. 1993. A short cut to deforestation. In _Functional programming languages and computer architecture: 6th conference_, 223-232. New York: ACM Press. - Lazy functional state threads John Launchbury and Simon L. Peyton Jones. 1994. Lazy functional state threads. In _PLDI '94: Proceedings of the ACM conference on programming language design and implementation_, vol. 29(6) of _ACM SIGPLAN Notices_, 24-35. New York: ACM Press. - Generic (polytypic) programming Ralf Hinze. 2000. A new approach to generic functional programming. In _POPL '00: Conference record of the annual ACM symposium on principles of programming languages_, 119-132. New York: ACM Press. Ralf Lämmel and Simon L. Peyton Jones. 2003. Scrap your boilerplate: A practical design pattern for generic programming. In _Proceedings of the 2003 ACM SIGPLAN international workshop on types in languages design and implementation_, 26-37. New York: ACM Press. - Data type invariants Chris Okasaki. 1999. From fast exponentiation to square matrices: An adventure in types. In _ICFP '99: Proceedings of the ACM international conference on functional programming_, vol. 34(9) of _ACM SIGPLAN Notices_, 28-35. New York: ACM Press. Ralf Hinze. 2001. Manufacturing datatypes. _Journal of Functional Programming_ 11(5): 493-524. Richard Bird and Ross Paterson. 1999. de Bruijn notation as a nested datatype. _Journal of Functional Programming_ 9(1): 77-91. Existential types are used in: - Object-oriented programming Benjamin C. Pierce and David N. Turner. 1994. Simple type-theoretic foundations for object-oriented programming. _Journal of Functional Programming_ 4(2): 207-247. Konstantin Läufer. 1996. Type classes with existential types. _Journal of Functional Programming_ 6(3): 485-517. - Abstract data types John C. Mitchell and Gordon D. Plotkin. 1988. Abstract types have existential type. _ACM Transactions on Programming Languages and Systems_ 10(3): 470-502. Any pointers or technique descriptions would be highly appreciated! If there are many contributions, I will post an updated version of this list. Ken -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig United Nations Day is 24 October. http://www.un.org/events/unday/ The Lost Voice of Radio Beijing http://www.milinfoserv.net/lvrb.html Write letters! We got half of New Testament that way.
In article <9jc531-5jc.ln1@proper.ptq.dyndns.org>, Ken Shan <ken@digitas.harvard.edu> wrote:
Norman Ramsey and I are looking for examples of where higher-rank polymorphism and existential types are useful. Can anyone think of uses besides the following?
I use HRP a fair amount. My most common use is in functions that convert structures to use different monads: remonadBigStruct :: (forall a. m1 a -> m2 a) -> BigStruct m1 -> BigStruct m2; I use existential types very occasionally: 1. when using types to represent compiled code, as in SQL: newtype Value t = MkValue String; Here the idea is that a "Value Int16" contains an SQL expression that will return a column of signed 16-bit values when used in a SELECT statement. Really I'm using the Haskell type-system as a stand-in for the essentially unrelated SQL type system. I build up Values in a special monad. But the function that turns that into an SQL statement needs a list of Values that may be of different types: getSQLSelect :: (Monad m) => SelectMonad m [Any Value] -> m String; data Any f = forall a. MkAny (f a); 2. Existential types also turn up in my implementation of the Scheme letrec function. This sort of thing is not normally allowed in Scheme: (letrec ( (a (cons 'x b)) (b (cons 'y a)) ) ...body... ) But Haskell is a lazy language, and I wanted to use that to extend letrec to allow lazy recursive construction of circular lists and the like, using mfix. But this is complicated by the fact that there may be any number of declarations in the head of the letrec form. I need some structure to be the argument type for my mfix. The existential type at the heart of my implementation is this: data MutualBindings f a v = forall t. (ExtractableFunctor t) => MkMutualBindings (t (f a)) (forall r. f r -> f (t v -> r)); The idea is that I want to represent n functions, each of which has n dependencies, for any n. "t" here is one of my fixed-length list types, depending on n: data ZeroList a = MkZeroList; data NextList t a = MkNextList a (t a); MutualBindings is used to represent the binding declarations in the head of the letrec form. In the example above, these would be (a (cons 'x b)) (b (cons 'y a)) Here there are two binding declarations, so n = 2, and the MutualBindings that gets built will use (NextList (NextList ZeroList)) for t. The first argument of the MutualBindings is therefore two expressions, corresponding to the Scheme expressions "(cons 'x b)" and "(cons 'y a)". The second part is an "abstracter" function that converts any expression on r into an expression on a function to r that takes a pair of variables, by abstracting on the Scheme symbols "a" and "b". The important thing is that I've made the type existential on "t" to say that I want the two ts the same, but I don't care which "t" it is. So if I have two expressions, then the abstracter must work on two symbols. If I have five expressions, then it must work on five symbols. And all I need to know about it is that it's an ExtractableFunctor, i.e. I have fmap and the function fExtract :: t (f a) -> f (t a); If my "a" type is in fact (IO SchemeObject) or somesuch, I can then use mfix to perform the letrec. Try it out at <http://hscheme.sourceforge.net/interpret.php> (define xyxy (letrec ((a (cons 'x b)) (b (cons 'y a))) a)) (list-head xyxy 30) -- Ashley Yakeley, Seattle WA
participants (2)
-
Ashley Yakeley -
Ken Shan