[Haskell] Applicative translucent functors in Haskell
Chung-chieh Shan
ccshan at post.harvard.edu
Mon Sep 13 15:20:33 EDT 2004
On 2004-09-08T19:46:55+0200, Tomasz Zielonka wrote:
> On Wed, Sep 08, 2004 at 04:27:23PM +0100, Simon Peyton-Jones wrote:
> > The ML orthodoxy says that it's essential to give sharing constraints by
> > name, not by position. If every module must be parameterised by every
> > type it may wish to share, modules might get a tremendous number of type
> > parameters, and matching them by position isn't robust. I think that
> > would be the primary criticism from a programming point of view. I have
> > no experience of how difficult this would turn out to be in practice.
> How about named fields in type constructors? Something like Haskell's
> records but at type level. Seems like a fun extension ;)
Proponents of ML-style module systems emphasize the advantage
of "sharing by specification" (or "fibration") over "sharing by
construction" (or "parameterization") (MacQueen 1986; Pierce 2000;
Harper and Pierce 2003). As Simon Peyton-Jones noted, in the context
of our translations of ML-style modules into System F-omega and
Haskell, sharing by specification gives type-equality constraints by
name, whereas sharing by construction gives type-equality constraints
by position. Harper and Pierce (2003; Pierce 2000) give examples of
modular programming where the latter approach can lead to an exponential
number of parameters, which are clumsy to deal with at best. It has
been often suggested that records at the type level be introduced to
address this issue (Jones 1995, 1996; Shao 1999a,b; Shan 2004; Tomasz
Zielonka in this discussion thread).
In this message, we (Oleg Kiselyov and Chung-chieh Shan) translate
Harper and Pierce's example into Haskell, using only the most common
Haskell extensions to give type-equality constraints by name and avoid
an exponential blowup. This exercise suggests that, while type-level
records may be convenient to have in Haskell, they may not be strictly
necessary to express sharing by specification. As shown below, we
can indeed refer to type parameters "by name", taking advantage of
the ability of a Haskell compiler to unify type expressions and bind
type variables. Our technique may be generalizable to encode all
sharing by specification. We hope this message helps clarify the
difference between the two sharing styles, and relate the ML and Haskell
orthodoxies.
First, let us demonstrate the exponential explosion of type variables.
We again will be using OCaml and Haskell in parallel, to make our
Haskell translation of module expression clearer. Later we shall
show how we prevent the exponential explosion in Ocaml -- and how
to translate that solution to Haskell. Again this message is a
doubly-literal code: both in OCaml and Haskell. It can be loaded in
GHCi or Hugs -98 as it is. To get the OCaml code, please filter the
text of the message with "sed -n -e '/^}/ s/^} //p'"
> {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
> module FNs where
(The final solution arrived at by the end of this message does not
require -fallow-undecidable-instances above.)
Let us consider a module of the following interface (a signature, in
ML speak):
} module type FN = sig
} type a
} type b
} val app : a -> b
} end
This is the interface of a regular function. It can be thought of
as a compiler stage or network protocol stack that translates one
intermediate language or representation (type a) into another (type b).
Here are two sample modules of that signature:
} module TIF = struct
} type a = int
} type b = float
} let app x = float_of_int x
} end
}
} module TFI = struct
} type a = float
} type b = int
} let app x = truncate x + 1
} end
In our Haskell translation, a signature corresponds to a type class,
and an implementation (a structure, aka module) to an instance:
> class NFN a b where
> napp:: a -> b
>
> instance NFN Integer Float where
> napp x = fromInteger x
>
> instance NFN Float Integer where
> napp x = truncate x + 1
Let us write a module that represents a composition appr . appl of
two FN-functions: appl: al->bl and appr: ar->br. In order for the
composition to be well-formed, the result type of appl must be the
argument type of appr: bl = ar (which we will call the intermediate
type t). Let us further suppose that we wish to make this intermediate
type explicit (e.g., for inspection, to resolve overloading, to invoke
the two intermediate functions separately, etc). Thus we arrive at the
following interface:
} module type NFN1 = sig
} type a1
} type t
} type b1
} val app1 : a1 -> b1
} end
Or, in Haskell
> class NFN1 a t b where
> napp1:: t -> a -> b
Note that the type of the intermediate result is really needed in
Haskell, to resolve the overloading and properly select the instance.
The composition of two modules of the signature FN is computed by the
following transparent functor:
} module NFn1(L: FN)(R: (FN with type a = L.b)) = struct
} type a1 = L.a
} type t = L.b
} type b1 = R.b
} let app1 x = R.app (L.app x)
} end
It takes two modules of the signature FN, labeled L and R. We should
note a _sharing constraint_: the type a of module R must be the same
as the type b of module L. The result of the NFn1 is a module of the
signature NFN1.
Here is an example of using the module
} module TIFI = NFn1(TIF)(TFI)
} let test_tifi = TIFI.app1 7;;
In Haskell, the functor corresponds to an instance with constraints
that correspond to the argument signatures. The sharing is expressed
by sharing of the names of type variables:
> instance (NFN a t, NFN t b) => NFN1 a t b where
> napp1 t x = napp (napp x `asTypeOf` t)
>
> test_nfn1::Integer
> test_nfn1 = napp1 (undefined::Float) (7::Integer)
Suppose we wish to compose two modules NFN1 again. Again, we wish to
expose all intermediate types
} module type NFN2 = sig
} type a2
} type tl type t type tr
} type b2
} val app2 : a2 -> b2
} end
}
} module NFn2(L: NFN1)(R: (NFN1 with type a1 = L.b1)) = struct
} type a2 = L.a1
} type tl = L.t
} type t = L.b1
} type tr = R.t
} type b2 = R.b1
} let app2 x = R.app1 (L.app1 x)
} end
We should note again that the functor NFn2 imports two modules of the
signature NFN1 and re-exports their types, after relabeling them to avoid
ambiguity and applying the sharing constraint R.a1 = L.b1.
In Haskell:
> class NFN2 a tl t tr b where
> napp2:: (tl,t,tr) -> a -> b
>
> instance (NFN1 a tl t, NFN1 t tr b) => NFN2 a tl t tr b where
> napp2 (tl,t,tr) x = napp1 tr $ ((napp1 tl x) `asTypeOf` t)
We can do that again:
} module type NFN3 = sig
} type a3
} type tl type t type tr
} type b3
} val app3 : a3 -> b3
} end
}
} module NFn3(L: NFN2)(R: (NFN2 with type a2 = L.b2)) = struct
} type a3 = L.a2
} type tll = L.tl
} type tl = L.t
} type trl = L.tr
} type t = L.b2
} type tlr = R.tl
} type tr = R.t
} type trr = R.tr
} type b3 = R.b2
} let app3 x = R.app2 (L.app2 x)
} end
In Haskell:
> class NFN3 a tll tl tlr t trl tr trr b where
> napp3:: ((tll,tl,tlr),t,(trl,tr,trr)) -> a -> b
>
> instance (NFN2 a tll tl tlr t, NFN2 t trl tr trr b)
> => NFN3 a tll tl tlr t trl tr trr b where
> napp3 (tl,t,tr) x = napp2 tr $ ((napp2 tl x) `asTypeOf` t)
Here is a usage example
} module TII = struct
} type a = int
} type b = int
} let app x = x + 2
} end
}
} module NM1 = NFn1(TII)(TII)
} module NM2 = NFn2(NM1)(NM1)
} module NM3 = NFn3(NM2)(NM2)
} let test_nm3 = NM3.app3 5;;
> instance NFN Integer Integer where
> napp x = x + 2
>
> test_nfn3:: Integer
> test_nfn3 = let i = undefined::Integer
> i3 = (i,i,i)
> in napp3 (i3,i,i3) (5::Integer)
The exponential explosion of the type variables is apparent. The term
expressions, the module expressions, and the sharing constraints are all
"linear". That is, if we wish to define another level of composition,
NFN4, we write an expression similar to NFn3, which, if we disregard the
type variables, has roughly the same size, in characters. It's only
when we look at the type variables we see the explosion. The explosion
can be overcome if could magically say: import module NFNn as L; import
module NFNn as R; make sure that L.bn = R.an; and re-export the rest.
Alas, we can't deal with the type variables of a structure 'in bulk'.
If we wish to re-export them, we have to enumerate them all.
The explosion is particularly apparent in Haskell, where we refer to
type parameters of a class by their position rather than by their name.
If we wish to write another level of composition, say, NFN4, we merely
need the first type variable NFN3 and the last type variable of NFN3.
Alas, we have to enumerate all the type variables in-between.
It turns out that we _can_ refer to type variables of a module "in
bulk", both in OCaml and in Haskell. To do that, we introduce a more
structural representation:
} module type FN1 = sig
} type a type b type t
} module ML : (FN with type a = a and type b = t)
} module MR : (FN with type b = b and type a = t)
} val app : a -> b
} end
}
} module Fn1(L: FN)(R: (FN with type a = L.b)) = struct
} type a = L.a type b = R.b type t = L.b
} module ML = L module MR = R
} let app x = R.app (L.app x)
} end
}
} module type FN2 = sig
} type a type b type t
} module ML : (FN1 with type a = a and type b = t)
} module MR : (FN1 with type b = b and type a = t)
} val app : a -> b
} end
}
} module Fn2(L: FN1)(R: (FN1 with type a = L.b)) = struct
} type a = L.a type b = R.b type t = L.b
} module ML = L module MR = R
} let app x = R.app (L.app x)
} end
The details of the two halves of the composition are stowed away in the
submodules ML and MR. We avoid the explosion in Ocaml because we can
mention, for example, the type tl in NFN2 above as ML.t in FN2 instead.
We can build a chain of functions using source code of size logarithmic
in the length of the chain.
Let us extend the chain one more time for illustration, and show an
example:
} module type FN3 = sig
} type a type b type t
} module ML : (FN2 with type a = a and type b = t)
} module MR : (FN2 with type b = b and type a = t)
} val app : a -> b
} end
}
} module Fn3(L: FN2)(R: (FN2 with type a = L.b)) = struct
} type a = L.a type b = R.b type t = L.b
} module ML = L module MR = R
} let app x = R.app (L.app x)
} end
}
} module M1 = Fn1(TIF)(TFI)
} module M2 = Fn2(M1)(M1)
} module M3 = Fn3(M2)(M2)
} let test_m3 = M3.app 5
With the help of Haskell type classes, we can also stow away the
detailed type information of a module.
First, we re-define our class representing the signature FN to take an
extra type parameter:
> class FN s a b | s -> a, s -> b where
> app:: s -> a -> b
The parameter 's' is a `label' that uniquely identifies an instance of
the class FN: in other words, the label 's' represents a module of a
signature FN. The label is a `proxy' for the module. Here are a few
examples of such modules:
> instance FN (Integer->Float) Integer Float where
> app _ x = fromInteger x
>
> instance FN (Float->Integer) Float Integer where
> app _ x = truncate x + 1
>
> instance FN (Integer->Integer) Integer Integer where
> app _ x = x + 2
>
> data L = L
> instance FN L Integer Integer where
> app _ x = x + 2
In the last example, we used an `artificial' label "L". Now we can
write the signature and the functor FN1 that `composes' FN once, the
signature FN2 and the corresponding functor that compose FN twice,
etc. However, because in Haskell an instance can refer to itself, we
can create a recursive functor and a signature:
> instance (FN u a t, FN v t b) => FN (u,v) a b where
> app s = app (snd s) . app (fst s)
The FN instance above subsumes the old classes NFN1, NFN2, NFN3, etc.,
all under the same FN class:
> fn'1 = undefined :: (Integer->Float, Float->Integer)
> fn'2 = (fn'1, fn'1)
> fn'3 = (fn'2, fn'2)
> test_fn' = app fn'3 5
If fn'1 is a 2-stage compiler, then fn'2 is a 4-stage compiler and
fn'3 is an 8-stage one. The types of fn'1, fn'2, fn'3 above grow
exponentially, just as the Ocaml signature FN2 above is twice the size
of FN1 when expanded out. But signature definitions in Ocaml and type
synonyms in Haskell allow us to avoid the explosion in the source code.
Even though the details of these composed modules are stowed away,
they are not hidden. Indeed, the label uniquely determines the the
module. We can inspect the label or its type to find sub-labels,
which uniquely describe the intermediate modules and their internal
types. For example, here is a Haskell function that runs the first 3
stages of an 8-stage compiler like fn'3:
> stages123of8 (_::((s12,(s3,s4)),s5678))
> = app (undefined::s3) . app (undefined::s12)
The type of stages123of8 is inferred to be
*FN> :t stages123of8
stages123of8 :: forall b a s5678 s4 s3 s12 b1.
(FN s12 a b1, FN s3 b1 b) =>
((s12, (s3, s4)), s5678) -> a -> b
Here ((s12,(s3,s4)),s5678) is a dummy type argument that identifies the
module (in other words, resolves the overloading). Note that the term
and type above only mentions the parts of the module that are actually
used, not the exponentially-sized details of say s5678. We thus avoid
exponential blowup and achieve sharing by specification.
> test_stagem3 = stages123of8 fn'3 5
*FN> :t test_stagem3
test_stagem3 :: Float
*FN> test_stagem3
6.0
We should point out that we have indeed accessed an intermediate type in
fn'3: although the whole compiler "app fn'3" maps Integer to Integer,
the first three stages map Integer to an intermediate type Float. We
have taken a great advantage of the pattern-matching ability of the
Haskell compiler: the ability to unify one type expression with the
other and bind type variables.
REFERENCES
Robert Harper, and Benjamin C. Pierce. 2003. Design issues in advanced
module systems. In Advanced topics in types and programming languages,
ed. Benjamin C. Pierce. Cambridge: MIT Press. Draft manuscript.
Mark P. Jones. 1995. From Hindley-Milner types to first-class structures.
In Proceedings of the Haskell workshop, ed. Paul Hudak. Tech. Rep. YALEU/
DCS/RR-1075, New Haven: Department of Computer Science, Yale University.
http://www.cse.ogi.edu/~mpj/pubs/haskwork95.pdf
http://www.cse.ogi.edu/~mpj/pubs/haskwork95.ps
http://www.cse.ogi.edu/~mpj/pubs/haskwork95.dvi.gz
Mark P. Jones. 1996. Using parameterized signatures to express modular
structure. In POPL '96: Conference record of the annual ACM symposium
on principles of programming languages, 68-78. New York: ACM Press.
http://www.cse.ogi.edu/~mpj/pubs/paramsig.html
http://www.cse.ogi.edu/~mpj/pubs/paramsig.pdf
http://www.cse.ogi.edu/~mpj/pubs/paramsig.ps
http://www.cse.ogi.edu/~mpj/pubs/paramsig.dvi.gz
David B. MacQueen. 1986. Using dependent types to express modular
structure. In POPL '86: Conference record of the annual ACM symposium
on principles of programming languages, 277-286. New York: ACM Press.
http://www.cs.bell-labs.com/who/dbm/papers/popl86/paper.ps
Benjamin C. Pierce. 2000. Advanced module systems: A guide for the
perplexed. ICFP invited talk.
http://www.cis.upenn.edu/~bcpierce/papers/modules-icfp.ps
Chung-chieh Shan. 2004. Higher-order modules in System F-omega and
Haskell. Draft manuscript.
http://www.eecs.harvard.edu/~ccshan/xlate/xlate.ps.gz
http://www.eecs.harvard.edu/~ccshan/xlate/xlate.pdf
Zhong Shao. 1999a. Transparent modules with fully syntactic signatures.
In ICFP '99: Proceedings of the ACM international conference on functional
programming, vol. 34(9) of ACM SIGPLAN Notices, 220-232. New York:
ACM Press.
http://flint.cs.yale.edu/flint/publications/fullsig.ps.gz
http://flint.cs.yale.edu/flint/publications/fullsig.pdf
Zhong Shao. 1999b. Transparent modules with fully syntactic signatures.
Tech. Rep. YALEU/ DCS/ TR-1181, Department of Computer Science, Yale
University, New Haven.
http://flint.cs.yale.edu/flint/publications/fullsig-tr.ps.gz
http://flint.cs.yale.edu/flint/publications/fullsig-tr.pdf
--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
2004-09-21 International Day of Peace http://www.un.org/events/peaceday/
________________________o.o________________________
Rich Zitola for Massachusetts State Senate (Worcester and Middlesex District)
http://www.vote-zitola.org/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org//pipermail/haskell/attachments/20040913/43d53b81/attachment-0001.bin
More information about the Haskell
mailing list