; Evaluation of this file yields an HTML document
; $Id: types.scm,v 1.34 2010/08/02 01:46:31 oleg Exp oleg $

(define Content
'(html:begin
  (Header
   (title "Haskell Programming: Types")
   (description "Less-than-traditional uses of types: dependent, higher-ranked, existential, etc. types and logical type programming")
   (Date-Revision-yyyymmdd "20100801")
   (Date-Creation-yyyymmdd "20030406")
   (keywords "Haskell, multiparameter classes, multivariate functions,
typeclass programming, existential types, higher-ranked types,
categorical products, dependent types, computations in types,
number-parameterized types")
   (AuthorAddress "oleg-at-okmij.org")
   (long-title "Haskell Programming: Attractive Types")
   (Links
    (start "index.html" (title "Haskell Programming"))
    (contents "index.html")
    (prev "index.html")
    (next "number-parameterized-types.html")
    (top "../README.html")
    (home "http://okmij.org/ftp/")))

  (body
   (navbar)
   (page-title)


;   (TOC)

(center
  (Cite "Haskell has become a laboratory and playground for advanced
type hackery") (br)
  "Simon Peyton Jones: Wearing the hair shirt: a retrospective on
Haskell. POPL 2003, invited talk.")


   (ul
     (li 
       (a (@ (name "keyword-args") (href "polyvariadic.html"))
	 "Polyvariadic functions and keyword arguments"))
     (li (local-ref "restricted-datatypes"))
     (li (a (@ (href "../Computation/lambda-calc.html#haskell-type-level"))
	   "Lambda-calculator on types"))
     (li (local-ref "computable-types"))
     (li (local-ref "partial-sigs")
       (br) (n_))

     (li (a (@ (name "monadic-regions") (href "regions.html"))
	   "Region-based resource management"))
     (li (local-ref "de-typechecker"))
     (li (local-ref "branding"))
     (li (local-ref "dependently-typed-append"))
     (li (local-ref "peano-arithm")
       (br) (n_))

     (li (local-ref "ls-resources"))
     (li (local-ref "binary-arithm"))
     (li (a (@ (href "number-parameterized-types.html"))
	   "Number-parameterized types and decimal type arithmetic"))
     (li (local-ref "unsound-typeable"))
     (li (local-ref "state-algebra")
       (br) (n_))

     (li (local-ref "Prepose"))
     (li (local-ref "class-based-dispatch"))
     (li (local-ref "class-based-overloading"))
     (li (a (@ (href "../Computation/Generative.html#diff-typeclass"))
	   "Type(class)-directed symbolic differentiation"))
     (li (a (@ (href "../Computation/Generative.html#diff-th"))
	   "Most optimal symbolic differentiation of compiled numeric
           functions")
       (br) (n_))

     (li (a (@ (name "is-function-type") (href "typecast.html"))
	   "Type improvement constraint, local functional dependencies,
and a type-level typecase"))
     (li (local-ref "poly2"))
     (li (local-ref "undecidable-inst-defense"))
     (li (a (@ (href "../ML/ML.html#typeclass")) 
	   "Typeclass overloading and bounded polymorphism in ML"))
     (li (local-ref "HList")
       (br) (n_))

     (li (a (@ (href "../Computation/monads.html#param-monad"))
	   "Variable (type)state `monad'"))
     (li "Type-safe printf and scanf: the "
       (a (@ (href "../typed-formatting/FPrintScan.html#DSL-In"))
	 "initial")
       " and the "
       (a (@ (href "../typed-formatting/FPrintScan.html#DSL-FIn"))
	 "final")
       " views")
     (li (local-ref "some-impredicativity"))
     (li (local-ref "fix"))
     (li (a (@ (href "generics.html"))
	   "Data-Generic and Data-Extensible Programming")
       (br) (n_))

     (li (a (@ (href "../tagless-final/tagless-typed.html#tc-GADT-tc"))
	   "Metatypechecking: "
	   "Staged Typed Compilation into GADT via typeclasses"))
     (li (local-ref "translucent-functor"))
     (li (local-ref "fibration"))
     (li (a (@ (href "../Scheme/xml.html#typed-SXML")) "Typed SXML"))
     (li (local-ref "stanamic-AVL"))
     (li (a (@ (href "../ML/ML.html#GADT"))
	   "GADT programming in OCaml"))
     (li (local-ref "Haskell1"))

     )

(p
  "Most code samples in this section require a Haskell extension to
multi-parameter classes with functional dependencies. Some examples
need an existential datatype extension. Both extensions are
commonly implemented. They can be activated by passing a flag " (code
"-fglasgow-exts") " to the Glasgow Haskell system GHC or GHCi, and a
flag " (code "-98") " to Hugs.")

   (p (hr))

;------------------------------------------------------------------------

(Description-unit "restricted-datatypes"
  "Restricted Monads"
  (body
    (p
      "We show how to attain the gist of the restricted datatype
proposal (Hughes, 1999) in Haskell, " (em "now") ". We need solely
multi-parameter type classes; no functional dependencies, no
undecidable instances, let alone more controversial extensions, are
required. Restricted monads thus should be implementable in
Haskell'.")
    (p
      "By definition, monadic operations such as 
" (code "return :: a -> m a") " and " (code "bind") " must be fully
polymorphic in the type of the value " (code "a") " associated with
the monadic action " (code "m a") ". Indeed, " (code "return") " must
be a natural transformation. A recurring discussion on Haskell mailing
lists points out the occasional need to restrict that
polymorphism. For example, one of the common implementations of MonadPlus
collects the choices, the results of non-deterministic computations, in a
list. One may wish for a more efficient data structure, such as
" (code "Data.Map") " or a " (code "Set") ". That however
requires the " (code "Ord") " constraint on the values, therefore,
neither Map nor Set may be instances of Monad, let alone
MonadPlus. More examples of restricted monads are discussed in the
article below.")

    (p "We propose a fully backward-compatible extension to the
monadic interface. All monads are members of the
extended monads, and all existing monadic code should compile as it
is. In addition, restricted monads become expressible. The article
defines the extended interface with the functions")
    (verbatim
      "ret2  :: MN2 m a   => a -> m a"
      "fail2 :: MN2 m a   => String -> m a"
      "bind2 :: MN3 m a b => m a -> (a -> m b) -> m b"
      )

"which have exactly the same type as the ordinary monadic operations
-- only with more general constraints. Because
new operations have exactly the same type, one may use them in the
regular monadic code (given -fno-implicit-prelude flag) and with the
do-notation (cf. `rebindable syntax' feature). Perhaps one day this
more general interface becomes the default one."

    (p "The gist of our proposal is the splitting of the Monad class into
two separate classes, " (code "MN2") " for " (code "return") " and
"(code "fail") " and " (code "MN3") " for " (code "bind") ". The
latter class implies the former. The new classes explicitly mention
the type of the monadic action value in their interface. That makes it
possible to attach constraints to those types. The article shows
the attaching of the " (code "Ord") " constraint, so to make Set an
instance of Monad and MonadPlus.")  )
  (version "1.1, Feb 8, 2006")
  (references
    (p
      (fileref "RestrictedMonad.lhs"
	"The literate Haskell source code and a few tests"
	(br)
	"The code was originally posted as "
	(Cite "Restricted Data Types Now")
	" on the Haskell' mailing list on Wed, 8 Feb 2006 00:06:23 -0800 (PST)"
	))
    (p (fileref "DoRestrictedM.hs"
	 "The illustration of the do-notation for restricted monads, which
	  works already for GHC 6.6 and later. We demonstrate that the
          do-notation works uniformly for ordinary monads and restricted monads.
          We show the conventional-looking monadic code which nevertheless
          uses " (code "Data.Set") " as the implementation
          of " (code "MonadPlus") " -- a frequently requested feature."))
    (p
      "John Hughes: Restricted datatypes in Haskell." (br)
      "Haskell 1999 Workshop, ed. Erik Meijer. Technical Report "
      "UU-CS-1999-28, Department of Computer Science, Utrecht University."
      (URL "http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps"))
      )
  )


(Description-unit "stanamic-AVL"
  "Polymorphic stanamically balanced AVL trees"
  (body
    (p
      "We describe a datatype of polymorphic balanced binary trees:
AVL trees. The trees are polymorphic: the values in different nodes
may have different type. The trees are balanced: for each non-leaf
node, the heights of its two children can differ at most by one.
Here, by definition the height of a node is 1 + max of the heights of
its children. A leaf node has the height of 0.")
    (p
      "The main feature of the present approach is a blended static
and dynamic enforcement of the balancing constraint. The function 
" (code "make_node") " verifies the balancing constraint at compile time
-- if it can. If the static check is not possible, the function delays
the check till the run-time.")
    (p
      "A detailed follow-up message by Chris Okasaki describes a very
interesting representation of AVL trees with the balancing constraint
ensured statically by a type-checker.")
    )
  (version "1.5, Apr 26, 2003")
  (references
    (p
      (fileref "stanamically-balanced-trees.lhs"
	"The literate Haskell source code and a few tests"
	(br)
	"The code was originally posted as "
	(Cite "Polymorphic stanamically balanced binary trees")
	" on Haskell mailing list on Sun, 20 Apr 2003 15:25:12 -0700 (PDT)"
	))
    (p "Christopher Okasaki. A follow-up message posted on 
Haskell mailing list on Mon, 28 Apr 2003 08:34:37 -0400"
      (URL 
	"http://www.haskell.org/pipermail/haskell/2003-April/011693.html")
      )))


(Description-unit "partial-sigs"
  "Partial signatures"
  (body
    (p
      "The regular (full) signature of a function specifies the type
of the function and -- if the type includes constrained type variables
-- enumerates " (em "all") " of the typeclass constraints. The list of
the constraints may be quite large. Partial signatures help when:")
    (ul
      (li "we wish to add an extra constraint to the type of the
function but we do not wish to explicitly write the type of the
function and enumerate all of the typeclass constraints,")
      (li "we wish to specify the type of the function and perhaps
some of the constraints -- and let the typechecker figure out the rest
of them."))
    (p "Contrary to a popular belief, both of the above are easily
possible, in " (em "Haskell98") ".")
    )
  (version "1.1, Aug 6, 2004")
  (references
    (fileref "partial-signatures.lhs"
      "The literate Haskell code with explanations and the examples"
      (br)
      "The code was originally posted as "
      (Cite "Partial signatures")
      " on Haskell-Cafe mailing list on Fri, 6 Aug 2004 20:29:40 -0700 (PDT)"
      )
    (p (a (@ (href "index.html#making-function-strict"))
	 "How to make a function strict without changing its body")
      (br) "Another application of the trick of adding a clause with an
always failing guard")
    )
  )



(Description-unit "branding"
  ("Eliminating Array Bound Checking through Non-dependent types")
  (body
    (p
      "There is a view that in order to gain static assurances such as an
array index being always in range or " (code "tail") " being applied to a
non-empty list, we must give up on something significant: on data
structures such as arrays (to be replaced with nested tuples), on
general recursion, on annotation-free programming, on clarity of code,
on well-supported programming languages. That does not have to be the
case. The present messages show non-trivial examples involving native
Haskell arrays, index computations, and general recursion. All arrays
indexing operations are statically guaranteed to be safe -- and so we
can safely use an efficient " (code "unsafeAt") " provided by GHC seemingly for
that purpose. The code is efficient; the static assurances cost us no
run-time overhead. The example uses only Haskell98 + higher-ranked
types. No new type classes are introduced. The safety is based on:
Haskell type system, quantified type variables, and a compact
general-purpose trusted kernel.")
    (p
      "This message has been inspired by the work of Hongwei Xi and
his initiated movement to make dependent-type programming
practical. The influence of his famous PLDI98 paper should be
obvious. We should note the parallels between dependent type
annotations in Hongwei Xi's Dependent SML code and the corresponding
Haskell code. What Hongwei Xi expressed in types, our code expressed
in terms. The terms were specifically designed in such a way so that
consequences of various tests be visible to the type system, and so
the corresponding conclusions could be propagated as part of the
regular type inference. There is a trusted kernel involved -- just as
the Dependent SML system has to be implicitly trusted. However, in the
given example the trusted kernel is a compact Haskell code plus the
GHC system. The latter is complex -- but it is being used by thousands
of people over extended period of time -- and so has higher confidence
than experimental extensions (unless the code of the latter has been
formally proven by a trusted system such as ACL2 or Coq).")
    (p "In the discussion thread, Conor T. McBride has made an
excellent summary of this approach and its relation to genuine
dependent types: ``The abstract " (code "brand") " is just a type-level
proxy for the bounding interval, and the library of operations
provides interval-respecting operations on indices. This is a very
neat solution in Haskell, but it goes round an extra corner which
isn't necessary with dependent types, where you can just talk about
the interval directly. The library-writer would develop and verify the
same convenient operations for working with intervals and indices; the
proofs would be independently recheckable terms in type theory.''")
    (p "Our most complex example is folding over multiple, 
" (em "variously-sized") " arrays.  This is like a fold over an array
-- generalized to an arbitrary number of arrays, whose lower and upper
index bounds may differ. The index ranges of some arrays do not even
have to overlap and may be empty. Neither the number of arrays to
process nor their index bounds are statically known. And yet we can
statically guarantee that whenever our code accesses any array
element, the index is certainly within the bounds of that
array. Typing this example in a genuinely dependent type system is
probably going to be quite challenging.")  )
  (references
    (p
      (fileref "eliminating-array-bound-check.lhs"
      "The literate Haskell code with explanations and the examples"
      (br)
      "The first version of the code was originally posted as "
      (Cite "Eliminating Array Bound Checking through Non-dependent types")
      " on the Haskell mailing list on Thu,  5 Aug 2004 19:31:36 -0700. "
      "The current version corrects the problem pointed out by Conor T.
McBride in the discussion thread." ))
    (p "Hongwei Xi and Frank Pfenning: "
      (Cite "Eliminating Array Bound Checking Through Dependent Types")
      " (PLDI'98)" (br)
      "The famous paper introducing practical dependent type system as
a dialect of SML. We faithfully re-implement the " (code "bsearch") "
example from that paper in Haskell98 plus higher-ranked types.")
    (p
      (textref "eliminating-array-bound-check-followup.txt"
	"Additional explanation of the branding technique"
	" and the response to the questions by Bjorn Lisper about the
relationship to classical range analyses known for a long time for
imperative languages. Verification of the library (perhaps using
Presburger solvers like the Omega Test by Bill Pugh) were also touched
upon.") (br)
      "The message was originally posted as "
      (Cite "Re: [Haskell] Eliminating Array Bound Checking through
Non-dependent types")
      " on the Haskell mailing list on Sun,  8 Aug 2004 16:50:33 -0700")

    (p
      (fileref "eliminating-mult-array-bound-check.lhs"
      (Cite "Eliminating Multiple-Array Bound Checking through
Non-dependent types") (br)
      "A message posted on the Haskell mailing list on Fri, 10 Feb 2006 22:05:04 -0800 (PST)."
	))


    (p (a (@ (href "number-parameterized-types.html"))
      "Number-parameterized types and decimal type arithmetic"))

    (p (a (@ (href "../Computation/lightweight-dependent-typing.html"))
	 "Lightweight Dependent-type Programming"))

    (p "Extensive discussion with Conor T. McBride, with his many
insights and explanations of dependent-type programming. Haskell
mailing list, August 6-9, 2004."
      (URL "http://www.haskell.org/pipermail/haskell/2004-August/014399.html")
      (URL "http://www.haskell.org/pipermail/haskell/2004-August/014403.html")
      (URL "http://www.haskell.org/pipermail/haskell/2004-August/014405.html"))

    (p (local-ref "dependently-typed-append"))
    )
)


(Description-unit "dependently-typed-append"
  ("Dependently-typed " (code "append"))
  (body
    (p
      "The subject of these article is ``heavier-weight''
dependent-type programming: using the type system to state and
guarantee non-trivial properties of terms. Unlike the lightweight
approach, we do not resort to a user-supplied trusted kernel: rather,
we exclusively rely on the type system.")
    (p "The poster problem for dependent types is to write a function
to append two lists that statically assures that the size of the
output list is the sum of the sizes of the two input lists. The lists must
therefore be described by a (dependent) type that carries the size of
the list.")
    (p "Martin Sulzmann, in a message on the Haskell list, has
posed the problem and gave its solutions:")
    (ul
      (li "with Hongwei Xi's DML or index types a la Christoph Zenger")
      (li "a Chameleon encoding of append in DML/index types")
      (li "an adaptation of an Omega example from Tim Sheard's papers;
the example can also run in Haskell + GADT")
      (li "proof-terms (equality terms) by Cheney, Hinze, Weirich, Xi et al."))
"Conor McBride showed the solution in Epigram. The present article
gives a Haskell solution, which makes an extensive use of partial
signatures and, in general, relies on the compiler to figure out the
rest of the constraints. We also separate the skeleton of the list
from the type of the list elements. Unlike the proof-term solution
given in Martin Sulzmann's message, we do not rely on any trusted
kernel (that is, the specially-constructed equality datatype " (code
"E") "). Rather, we base our trust on the Haskell type system only."
    (p
      "The solutions demonstrate two different levels of dependent
typing. In both cases, we formulate the desired properties using
dependent types, and attach them as signatures to functions.  We may
regard these dynamically-typed signature as ``compile-time
assertions''. If the use of our function in a particular expression
violates the assertion, the expression is flagged as ill-typed.  In a
semi-dynamic case, a run-time check is inserted. If a program
compiled, it does not mean that append truly respects the sum-of-sizes
constraint.  It merely means that in this particular compilation unit,
all the uses of append were statically found to respect the length
constraint. The more powerful approach, exhibited in Epigram, is to
say that in " (em "all") " possible compilations " (code "append") "
shall be found to satisfy the length constraint.")
  (p "Thus, at one level of dependent typing, assertions about a
particular function are checked at the " (em "usage") " occurrences of
that function, within the particular context of those occurrences. A
far more stronger level of dependent typing guarantees that the
assertions hold universally, in all possible contexts. That level
checks the " (em "definition") " of the function. The
difference between the levels is akin to the difference between
`dynamic' and `static' typing, but only at the compile-time.")
    (p "Both approaches are useful. Incidentally, GHC already does
``dynamic kinding'' with respect to typeclass instances: the mere fact
that a program unit has compiled does not assure us that all defined
instances are problem-free (e.g., non-overlapping). It simply means
that the uses of instances " (em "within the programming unit") " in
question were problem-free.")
  )
  (references
    (p
      (fileref "dependently-typed-append.lhs"
      "The literate Haskell code with explanations and the examples"
      (br)
      "The first version of the code was posted as "
      (Cite "Re: Dependent Types in Haskell")
      " on the Haskell mailing list on Sat, 14 Aug 2004 03:10:04 -0700."))

    (p "Martin Sulzmann: Dependent Types in Haskell" 
      (URL "http://www.haskell.org/pipermail/haskell/2004-August/014407.html")
      (URL "http://www.haskell.org/pipermail/haskell/2004-August/014408.html")
      (br) "Messages on the Haskell mailing list posted on
Wed Aug 11 2004.")

    (p "Conor T McBride: Dependent Types in Haskell" 
      (URL "http://www.haskell.org/pipermail/haskell/2004-August/014412.html")
      (br) "Message on the Haskell mailing list posted on
Wed Aug 11 05:00:25 EDT 2004.")
    (p (local-ref "branding"))
))




(Description-unit "de-typechecker"
  ("Reversing Haskell typechecker: converting from " (code "undefined") " to defined")
  (body
    (p
      "This message shows how to make the Haskell typechecker work in reverse:
to infer a term of a given type:")
    (verbatim
      "rtest4 f g = rr (undefined::(b -> c) -> (a -> b) -> a -> c) HNil f g"
      "*HC> rtest4 (:[]) Just 'x'"
      "[Just 'x']"
      "*HC> rtest4 Just Right True"
      "Just (Right True)"
      )
    (p
  "We ask the Haskell typechecker to derive us a function of the
specified type. We get the real function, which we can then apply to
various arguments. The return result does behave like a `composition'
-- which is what the type specifies. Informally, we converted from
" (code "undefined") " to defined.")
    (p
      "It must be emphasized that no modifications to the Haskell
compiler are needed, and no external programs are relied upon. In
particular, however surprising it may seem, we get by without " (code
"eval") " -- because Haskell has reflexive facilities already
built-in.")

    (p
      "Our system solves type habitation for a class of functions with
polymorphic types. From another point of view, the system is a prover
in the implication fragment of intuitionistic logic. Essentially we
turn a " (em "type") " into a logical program -- a set of Horn clauses -- which
we then solve by SLD resolution.  It is gratifying to see that
Haskell typeclasses are up to that task.")

    (p
      "The message below presents two different converters from a type
to a term.  Both derive a program, a term, from its specification, a
type -- for a class of fully polymorphic functions. The first
converter has just been demonstrated.  It is quite limited in that the
derived function must be used `polymorphically' -- distinct type
variables must be instantiated to different types (or, the user should
first instantiate their types and then derive the term). The second
converter is far more useful: it can let us `visualize' what a
function with a particular type may be doing.  For example, it might
not be immediately clear what is the function of the type")
    (verbatim
 "(((a -> b -> c) -> (a -> b) -> a -> c) -> (t3 -> t1 -> t2 -> t3) -> t) -> t)"
      )

"Our reifier says,"

    (verbatim
      "test9 = reify (undefined::(((a -> b -> c) -> (a -> b) -> a -> c) -> "
      "                            (t3 -> t1 -> t2 -> t3) -> t) -> t) gamma0"
      "*HC> test9"
      "\\y -> y (\\d h p -> d p (h p)) (\\d h p -> d)"
      )

"that is, the function in question is one of the X combinators. It is
an improper combinator. Similarly the reifier can turn a point-free
function into the pointful form to help really understand the
former. For example, it might take time to comprehend the following
expression:"

    (verbatim
"pz = (((. head . uncurry zip . splitAt 1 . repeat) . uncurry) .) . (.) . flip"
  )
"Our system says"
    (verbatim
      "test_pz = reify (undefined `asTypeOf` pz) gamma0"
      "*HC> test_pz"
      "\\h p y -> h y (p y)"
      )

"So, " (code "pz") " is just the S combinator."

    (p "An attempt to derive a term for the type " (code "a->b") "
expectedly fails. The type error message essentially says that " (code
"a |- b") " is underivable.")

    (p
      "The examples above exhibit fully polymorphic types -- those
with " (em "uninstantiated") ", implicitly universally quantified type
variables. That is, our typeclasses can reify not only types but also
type schemas. The ability to operate on and compare " (em "unground") " types
with " (em "uninstantiated") " type variables is often sought but rarely
attained. The contribution of this message is the set of primitives
for nominal equality comparison and deconstruction of unground
types.")
    )
  (version "1.1, Mar 1, 2005")
  (references
    (p (fileref "de-typechecker.lhs"
      "The literate Haskell code with extensive explanations and many
examples, including the code and explanation for the Equality
predicate on type schemas."
	 (br)
      "The code was originally posted as "
      (Cite "De-typechecker: converting from a type to a term")
      " on the Haskell mailing list on Tue,  1 Mar 2005 00:13:08 -0800 (PST)"
      ))
  (p
   "Lennart Augustsson: Announcing Djinn, version 2004-12-11, a coding wizard"
    (URL "http://www.haskell.org/pipermail/haskell/2005-December/017055.html")
    (br)
    "A Message posted on the Haskell mailing list on Sun Dec 11
17:32:07 EST 2005." (br)
    "The user types a Haskell type at DJinn's prompt, and DJinn gives
back a term of that type if one exists. The produced term is in
DJinn's term language. The printed term can be cut and pasted into the
Haskell code.")
  (p (fileref "pointless-translation.lhs"
    "The literate Haskell98 code for translating proper linear
combinators into point-free style."
       (br)
       "The code was originally posted as "
       (Cite "Automatic pointless translation")
       " on the Haskell-Cafe mailing list on Mon, 14 Feb 2005 22:56:04
-0800 (PST)")
    ))
)


(Description-unit "Prepose"
  "Implicit configurations -- or, type classes reflect the values of types"
  (body
    (p
      "The configurations problem is to propagate run-time preferences
throughout a program, allowing multiple concurrent configuration sets
to coexist safely under statically guaranteed separation.  This
problem is common in all software systems, but particularly acute in
Haskell, where currently the most popular solution relies on unsafe
operations and compiler pragmas.")
    (p
      "We solve the configurations problem in Haskell using only
stable and widely implemented language features like the type-class
system.  In our approach, a term expression can refer to run-time
configuration parameters as if they were compile-time constants in
global scope.  Besides supporting such intuitive term notation and
statically guaranteeing separation, our solution also helps improve
the program's performance by transparently dispatching to specialized
code at run-time.  We can propagate any type of configuration
data -- numbers, strings, " (code "IO") " actions, polymorphic functions,
closures, and abstract data types.  No previous approach to
propagating configurations implicitly in any language provides the
same static separation guarantees.")
    (p
      "The enabling technique behind our solution is to propagate
values via types, with the help of polymorphic recursion and
higher-rank polymorphism. The technique essentially emulates local
type-class instance declarations while preserving coherence.
Configuration parameters are propagated throughout the code implicitly
as part of type inference rather than explicitly by the programmer.
Our technique can be regarded as a portable, coherent, and intuitive
alternative to implicit parameters.  It motivates adding local
instances to Haskell, with a restriction that salvages principal
types.")
    (p "Joint work with Chung-chieh Shan.")
    )
  (version "1.1, Aug 2004")
  (references
    (URL "http://www.eecs.harvard.edu/~ccshan/prepose/")
    (p (a (@ (href "http://doi.acm.org/10.1145/1017472.1017481"))
	 "Proceedings of the ACM SIGPLAN 2004 workshop on Haskell") (br)
      "Snowbird, Utah, USA -- September 22, 2004 -- 
ACM Press, pp. 33 - 44.")
    (p "Expanded version: Technical report TR-15-04, Division of
Engineering and Applied Sciences, Harvard University."))
  )

(Description-unit "HList"
  "Strongly typed heterogeneous collections"
  (body
    (p
      "A heterogeneous collection is a datatype that is capable of
storing data of different types, while providing operations for
look-up, update, iteration, and others. There are various kinds of
heterogeneous collections, differing in representation, invariants,
and access operations. We describe HList --- a Haskell library for
strongly typed heterogeneous collections including extensible
records. We illustrate HList's benefits in the context of type-safe
database access in Haskell. The HList library relies on common
extensions of Haskell 98. Our exploration raises interesting issues
regarding Haskell's type system, in particular, avoidance of
overlapping instances, and reification of type equality and type
unification.")
    (p "Joint work with Ralf Laemmel and Keean Schupke.")
    )
  (version "1.1, Aug 2004")
  (references
    (URL "http://hackage.haskell.org/package/HList")
    (URL "http://code.haskell.org/HList/")
    (URL "http://homepages.cwi.nl/~ralf/HList/")
    (p (a (@ (href "http://doi.acm.org/10.1145/1017472.1017488"))
	 "Proceedings of the ACM SIGPLAN 2004 workshop on Haskell") (br)
      "Snowbird, Utah, USA -- September 22, 2004 -- 
ACM Press, pp. 96 - 107.")
    (p "Expanded version: CWI Technical report SEN-E0420, ISSN 1386-369X,
CWI, Amsterdam, August 2004."))
  )

(Description-unit "peano-arithm"
  "Class-parameterized classes, and the type-level logarithm"
  (body
    (p
      "We show invertible, terminating, 3-place addition,
multiplication, and exponentiation relations on type-level unary, Peano
numerals, where " (em "any") " two operands determine the third. We
also show the invertible factorial relation. This gives us all common
arithmetic operations on Peano numerals, including n-base discrete
logarithm, n-th root, and the inverse of factorial. The latter
operations and division are defined generically, as inverses of
exponentiation, factorial and multiplication, resp. It takes only a
couple of lines to define each. The inverting method can work with any
representation of (type-level) numerals, binary or decimal.")
    (p
      "The inverter itself is generic: it is a type-class
" (em "function") ", that is, a type-class parameterized by the type-class to
`invert'. The inverter is a simple " (em "higher-order for-loop on types") 
". There has been a proposal on Haskell' to give equal rights
to types and classes.  In Haskell98+multi-parameter type classes,
classes are already first-class, for all practical purposes. We can
easily define (potentially, higher-order) type functions on type
classes.")
    (p "It becomes relatively straightforward then to implement RSA in types. 
That prompted Graham Klyne to remark on Haskell Cafe ``
 Methinks this gives a whole new meaning to \"type security\"''")
    )
  (version "1.1, Feb 2, 2006")
  (references
    (fileref "PeanoArithm.lhs"
	"The literate Haskell source code with tests"
	(br)
	"The code was originally posted as "
	(Cite "Class-parameterized classes, and the type-level logarithm")
	" on the Haskell mailing list on Thu, 2 Feb 2006 22:42:08 -0800 (PST)"
	))
      )


(Description-unit "binary-arithm"
  "Binary type arithmetic"
  (body
    (p "We introduce the type-level Haskell library for arbitrary
precision binary arithmetic over natural " (em "kinds") ". The library
supports addition/subtraction, predecessor/successor,
multiplication/division, exp2, all comparisons, GCD, and the maximum.
At the core of the library are multi-mode ternary " (em "relations") "
" (code "Add") " and " (code "Mul") " where " (em "any") " two
arguments determine the third. Such relations are especially suitable
for specifying static arithmetic constraints on computations. The
type-level numerals have no run-time representation; correspondingly,
all arithmetic operations are done at compile time and have no effect
on run-time.")

    (p "Here are the definitions of the well-formedness condition on
binary type numerals -- " (em "the kind predicate") " -- and of a few
operations on them:")

    (verbatim
      "class Nat0 a where toInt :: a -> Int"
      "class Nat0 a => Nat a                   -- (positive) naturals"
      "class (Nat0 x, Nat y) => Succ x y | x -> y, y -> x"
      "-- GCD over natural _kinds_"
      "class (Nat0 x, Nat0 y, Nat0 z) => GCD x y z | x y -> z"
      )

    "The numerals are specified in the familiar big-endian bit
notation. The sequence of " (code "B0") "s and " (code "B1") "s is the
bit-string of the number, whereas the number of " (code "U") "s is the
binary logarithm."

    (verbatim
      "type N2 = U B1 B0;               nat2 = undefined::N2"
      "type N4 = U (U B1 B0) B0;        nat4 = undefined::N4"
      "add :: Add x y z => x -> y -> z; add = undefined"
      "sub :: Add x y z => z -> x -> y; sub = undefined"
      "mul :: Mul x y z => x -> y -> z; mul = undefined"
      "div :: Mul x y z => z -> x -> y; div = undefined"
      ""
      "*BinaryNumber> :type mul (add nat2 nat4) (succ nat2)"
      "mul (add nat2 nat4) (succ nat2) :: U (U (U (U B1 B0) B0) B1) B0"
      "*BinaryNumber> :type div (add nat2 nat4) (succ nat2)"
      "div (add nat2 nat4) (succ nat2) :: U B1 B0"
      "*BinaryNumber> :type gcd (add nat2 nat4) (succ nat2)"
      "gcd (add nat2 nat4) (succ nat2) :: U B1 B1"
      )

    "We stress that all multiplication, GCD, etc. computations above are
performed as part of type checking: the reported numeral is the " (em
"type") " of the expression. The expression's value is " (code
"undefined") ": despite the familiar term-level notation,
expressions like " (code "(add nat2 nat4)") " are meant to be
evaluated at compile time and have no executable content. Also despite
the familiar functional term-level notation, the type computations are
invertible. We may ask, for example, what must be the type 
of " (code "x") " such that multiplying it by three gives six:"

    (verbatim
      "x = undefined where _ = mul x (succ nat2) `asTypeOf` (add nat2 nat4)"
      "*BinaryNumber> :type x"
      "x :: U B1 B0"
      )
    (p
      "We used the arithmetic type library to statically enforce validity,
range, size, and alignment constraints of raw memory pointers, and to
statically enforce protocol and time-related constraints when
accessing device registers. Our paper `Lightweight static resources'
describes the arithmetic type library, type-level records, type-level
programming with regular Haskell terms, and two sample
applications.")
    (p "Joint work with Chung-chieh Shan.")
    )
  (version "1.1, Feb 2, 2007")
  (references
    (p (fileref "../Computation/resource-aware-prog/BinaryNumber.hs"
	"The commented Haskell source code with tests"))
    (p (local-ref "ls-resources")))
  )


(Description-unit "ls-resources"
  "Lightweight static resources, for safe embedded and systems programming"
  (body
    (p "[The abstract]" (br)
      "It is an established trend to develop low-level code --
embedded software, device drivers, and operating systems -- using
high-level languages, especially functional languages with advanced
facilities to abstract and generate code.  To be reliable and secure,
low-level code must correctly manage space, time, and other resources,
so special type systems and verification tools arose to regulate
resource access statically. However, a general-purpose functional
language practical today can provide the same static assurances, also
without run-time overhead.  We substantiate this claim and promote the
trend with two security kernels in the domain of device drivers:")
    (ul
      (li "one built around raw pointers, to track and arbitrate the
size, alignment, write permission, and other properties of memory
areas across indexing and casting;")
      (li "the other built around a device register, to enforce
protocol and timing requirements while reading from the register."))
    "Our style is convenient in Haskell thanks to custom kinds and
predicates (as type classes); type-level numbers, functions, and
records (using functional dependencies); and mixed type- and
term-level programming (enabling partial type signatures)."
    (p "Joint work with Chung-chieh Shan.")
    )
  (version "1.1, Feb 2, 2007")
  (references
    (p (fileref "../Computation/resource-aware-prog/tfp.pdf"
	"Proc. Trends in Functional Programming. New York, Apr 2-4, 2007."))
    (p "Chung-chieh Shan: TFP 2007 talk, Apr 3, 2007."
      (URL "http://www.cs.rutgers.edu/~ccshan/tfp2007/talk.pdf"))
    (p (fileref "../Computation/resource-aware-prog/BinaryNumber.hs"
	 "Representation of binary numbers and arithmetic relations"))
    (p (fileref "../Computation/resource-aware-prog/Areas.hs"
	 "Strongly typed memory areas. The implementation of the library"))
    (p (fileref "../Computation/resource-aware-prog/AreaTests.hs"
	 "Sample strongly typed memory areas and examples of type records"))
    (p (fileref "../Computation/resource-aware-prog/VideoRAM.hs"
	 "Extensive example of strongly typed memory areas: safe and efficient
       access to videoRAM, with casts, pointer arithmetic and iterations"))
    (p (fileref "../Computation/resource-aware-prog/RealTime.hs"
	 "Statically tracking ticks: enforcing timing and protocol
restrictions when writing device drivers and their generators"))
))


; 


(Description-unit "class-based-overloading"
  "Choosing a type-class instance based on the context"
  (body
    (p
      "Type classes let us overload operations based on the type of an
expression. A frequently expressed wish is to overload based on the
class to which expression's type belongs. For example, we want to
define an overloaded operation " (code "print") " to be equivalent to 
" (code "(putStrLn . show)") " when applied to showable expressions,
whose types are the members of the class " (code "Show") ". For other
types, the operation " (code "print") " should do something
different (e.g., print that no show function is available, or, for
Typeable expressions, write their type instead).")
    (p "The naive approach clearly does not work")
    (verbatim
      "instance Show a => Print a where"
      "  print x = putStrLn (show x)"
      "instance        Print a where"
      "  print x = putStrLn \"No show method\""
      )
    "because the two instances have the identical heads " (code "Print
a") " and so considered duplicates by the type-checker. The WikiPage
below describes the working solution, relying on multi-parameter type
classes with functional dependencies and the type level predicate
describing the membership in the class Show. The trick is to re-write
a constraint " (code "(C a)") " which succeeds of fails, into a
predicate constraint " (code "(C' a flag)") ", which always succeeds,
but once discharged, unifies " (code "flag") " with a type-level
Boolean " (code "HTrue") " or " (code "HFalse") "."
    (p "Joint work with Simon Peyton-Jones.")
    )
  (version "1.1, April 2008")
  (references
    (p
      "The WikiPage with the explanation of the technique and of its several
variations"
      (URL "http://haskell.org/haskellwiki/GHC/AdvancedOverlap"))
    (p (a (@ (href "typecast.html"))
	 "Type improvement constraint, local functional dependencies,
and a type-level typecase") (br)
      "The method for defining type-level predicates")
    (p (local-ref "class-based-dispatch") (br)
      "A more `dynamic' solution")
    (p (local-ref "poly2") (br)
      "An example of building classes of types and defining their
membership predicate"))
)

(Description-unit "Haskell1"
  "Haskell with only one typeclass"
  (body
    (p
      "We demonstrate that removing from Haskell the ability to define
typeclasses leads to no loss of expressivity. Haskell restricted to a
single, pre-defined typeclass with only one method can express
all of Haskell98 typeclass programming idioms including constructor
classes, as well as multi-parameter type classes and even some functional
dependencies. The addition of TypeCast as a pre-defined constraint
gives us all functional dependencies, bounded existentials, and even
associated data types. Besides clarifying the role of typeclasses as
method bundles, we propose a simpler model of overloading resolution
than that of Hall et al.")
    (p
      "The article below introduces a subset of Haskell (called
Haskell1) with only one, pre-defined typeclass " (code "C") " with
only one method " (code "ac") ". We can add more instances
to " (code "C") " but cannot define any more typeclasses or any more
methods. Despite the restriction, we implement overloaded numerical
functions, " (code "show") " and, " (code "minBound") ". We define
monads and their extension, restricted monads.  We can define monad
transformers, e.g., " (code "MonadError") ", demonstrating that
Haskell1 supports some functional dependencies.")
    (p
      "To represent the rest of functional dependencies, we
introduce Haskell1' as an extension of Haskell1 with a pre-defined
constraint TypeCast (which is not user-extensible and can be regarded
built-in). We implement in Haskell1' the motivating example from the
paper `Associated Types with Class' by Chakravarty, Keller, Peyton
Jones and Marlow (POPL2005).  Finally we introduce the analogue of
Haskell98 classes -- method bundles -- and use them for defining
bounded existentials.")
    (p
      "Haskell1 is not a new language and requires no new
compilers. It is merely a subset of Haskell; the `removal' of
typeclass declarations is a matter of discipline rather than that of
syntax.")
    (p
      "Gerrit van den Geest has kindly pointed out another re-design
of Haskell type classes: System O of Odersky, Wadler, and Wehr. System
O however imposes the restriction that each function overloaded over
the type " (code "a") " must have the type of the form " (code "a ->
t") ", with " (code "a") " not free in " (code "t") ". Therefore,
System O cannot express, for example, " (code "fromInteger") " and
"(code "minBound") ". Haskell1 has no such restrictions and can
express any overloaded function of Haskell. Restricting Haskell to
only one particularly chosen typeclass is no restriction at all.")
    )
  (version "1.1, February 2007")
  (references
    (p
      (textref "Haskell1/Haskell1.txt"
	"The complete article")
      "It was originally posted"
	" on the Haskell mailing list on Wed, 28 Feb 2007 23:56:47 -0800 (PST)"
	)
    (p
      (fileref "Haskell1/Class1.hs"
	"Expressing Haskell98 typeclass idioms in Haskell1"))
    (p
      (fileref "Haskell1/Class2.hs"
	"Haskell1' and its expressivity") (br)
      "In addition to the single, pre-defined class " (code "C") ", we 
assume TypeCast.
The latter is not user-extensible and may be regarded as a pre-defined
constraint. To define TypeCast however, we need the undecidable instances
extension. Nothing else requires this extension; furthermore, TypeCast is
closed and non-recursive and so is certainly decidable.")
    (p (local-ref "restricted-datatypes"))
    ))


(Description-unit "poly2"
  "Type-class overloaded functions: second-order typeclass programming
with backtracking"
  (body
    (p
      "We demonstrate functions polymorphic over classes of types. Each
instance of such (2-polymorphic) function uses ordinary 1-polymorphic
methods, to generically process values of many types, members of that
2-instance type class. The typeclass constraints are thus manipulated
as first-class entities. We also show how to write typeclass instances
with back-tracking: if one instance does not apply, the typechecker
will chose the `next' instance -- in the precise meaning of
`next'.") 
    (p
      "We show a method to describe classes of types in
a " (em "concise")" way, using unions, class differences and
unrestricted comprehension. These classes of types may be either
closed or open (extensible). After that set up, we can write
arbitrarily many functions overloaded over these type classes. An
instance of our function for a specific type class may use polymorphic
functions to generically process all members of that type class. Our
functions are hence second-order polymorphic.")  )
  (version "1.1, November 2006")
  (references
    (p
      (textref "poly2.txt"
	"The complete article with explanations"
	"It was originally posted"
	" on the Haskell mailing list on Sun, 19 Nov 2006 16:54:34 -0800 (PST)"
	))
    (p
      (fileref "poly2.hs"
	"The complete Haskell source code"))
    (p
      (fileref "is-of-class.hs"
	"Small self-containing example of classifying data based on their types"
	(br)
	"This self-contained code defines
the function " (code "is_of_class")" to statically check if an object of
the type " (code "x") " is a member of the class " (code "c") ". A class
of types is defined by enumeration, set-union, set-difference, and unrestricted
comprehension."
	(br)
	"The code was originally posted as "
	(Cite "Re: Trying to avoid duplicate instances")
	" on the Haskell-Cafe mailing list Tue, 13 May 2008 23:04:29
-0700 (PDT)" ))
    ))

(Description-unit "class-based-dispatch"
  "Dynamic dispatch on a class of a type"
  (body
    (p
      "This message gives an example of a dynamic type " (em "class")
" cast in Haskell. We want to dispatch on a class of a type rather on
a type itself. In other words, we would like to simulate " (code
"IsInstanceOf") ". The problem was originally posed by Hal Daume III,
who wrote on the Haskell mailing list:")
    (blockquote
      "i'm hoping to be able to simulate a sort of dynamic dispatch
based on class instances.  basically a function which takes a value
and depending on what classes it is an instance of, does
something. I've been trying for a while to simulate something along
the lines of:"
      (verbatim
	"class Foo a where { foo :: a -> Bool }"
	"class Bar a where { bar :: a -> Bool }"
	"foo x"
	"  | typeOf x `instanceOf` Foo = Just (foo x)"
	"  | typeOf x `instanceOf` Bar = Just (bar x)"
	"  | otherwise                 = Nothing"))
    (p
      "The following code shows how to implement a dynamic dispatch on a type
class context. No unsafe operations are used. The test at the end
demonstrates that we can indeed simulate Hal's desired example.")
    )
  (version "1.1, Mar 23, 2003")
  (references
    (p

      (fileref "class-based-dispatch.lhs"
	"The literate Haskell source code and a test"
	(br)
	"The code was originally posted as "
	(Cite "simulating dynamic dispatch")
	" on the Haskell mailing list on Sun, 23 Mar 2003 13:41:48"
	))
    (p "Hal Daume III. simulating dynamic dispatch. The message with
the statement of the problem, posted on the Haskell mailing list on on Mar
20, 2003."
      (URL 
	"http://www.haskell.org/pipermail/haskell/2003-March/011518.html")
      )
    (p (local-ref "class-based-overloading") (br) "An alternative: a " 
      (em "static") " dispatch on a class of a type")
))



(Description-unit "undecidable-inst-defense"
  ("In defense of UndecidableInstances")
  (body
    (p 
      "Class instance and type family instance declarations are
subject to a set of strict conditions: Paterson and Coverage
Conditions for class instances (Section 7.6.3. ``Instance
declarations'' of GHC User's Guide, version 6.10.4) and similar
conditions for type families (Section 7.7.2.2.3. ``Decidability of
type synonym instances''). The conditions ensure that the process of
resolving class constraints or normalizing type function applications
always terminates.")
    (p
      "The conditions are quite constrictive, and GHC offers a way to
lift them, with the " (code "LANGUAGE") "
pragma " (code "UndecidableInstances") ". The pragma is shunned
however. There are good reasons for that attitude: if we lift the
conditions, we can write instances that send the type checker into
infinite loop (albeit only potentially: the termination is insured by
the recursion depth limit, set by the flag " (code "-fcontext-stack") ").
Section 7.6.3.2.  ``Undecidable instances'' describes two such (quite
subtle) cases.")
    (p
      "It is also true that Paterson and Coverage Conditions are
sufficient but by no means necessary to ensure the decidability of type
normalization. There are patently total type functions 
rejected by the Conditions. This article shows a simple
example, and argues for more acceptance towards
" (code "UndecidableInstances") ". The extension is not always bad,
and should not be automatically frowned upon.")
    (p
      "Our example is simple indeed:")
    (verbatim
      "{-# LANGUAGE TypeFamilies #-}"
      ""
      "type family I x :: *"
      "type instance I x = x"
      ""
      "type family B x :: *"
      "type instance B x = I x"
      )
"The code is not accepted by GHC 6.8.3 and GHC 6.10.4. The compiler complains:"
    (verbatim
      "Application is no smaller than the instance head"
      "  in the type family application: I x"
      "(Use -fallow-undecidable-instances to permit this)"
      "In the type synonym instance declaration for `B'"
      )
"Yet there cannot possibly be any diverging reduction sequence here!
The type family " (code "I") " is the identity, and the type
family " (code "B") " is its alias. There is no recursion. The fact
that type families are open is not relevant: type families in our code
are effectively closed, because one cannot define any more instance
for " (code "I") " and " (code "B") " (or risk overlap, which is
rightfully not supported for type families)."
    (p
      "GHC complains because it checks termination
instance-by-instance. To see the termination in the above type
program, we should consider the instances " (code "I") "
and " (code "B") " together. Then we will see that " (code "I") " does
not refer to " (code "B") ", so there are no loops. This global
termination check -- for a set of instances -- is beyond the abilities
of GHC. One may argue that this is the right decision: after all, GHCi
is not a full-blown theorem prover.")
    (p
      "Thus there are patently decidable type programs that require
" (code "UndecidableInstances") ". That extension should not be categorically
stigmatized.")
    (p "In conclusion, "
      (code "UndecidableInstances") " is not a dangerous flag. It will
never cause the type-checker to accept a program that `goes wrong.'
The only bad consequence of using the flag is type checker's might be
telling us that it cannot decide if our program is well-typed, given
the context-stack--depth limit. We may ask the type-checker to try a
bit harder (with a larger depth limit), or look through our program
and find the problem.")
    (p (code "UndecidableInstances") " is quite like to the primitive
recursion criterion: all primitive recursion functions surely
terminate; non-primitive recursion functions generally don't. Still
there are many classes of non-primitive recursive functions that are
total. To see their totality, one has to use more complex criteria.")  
))
; Haskell-Cafe Date: Wed, 14 Oct 2009 20:49:14 +0200


(Description-unit "fix"
  ("Many ways to the fix-point combinator besides the value recursion")
  (body
    (p 
"Value-level recursion in Haskell is built-in since  
definitions are implicitly recursive. The explicit polymorphic 
fix-point combinator can therefore be defined simply as")
    (verbatim
      "fix :: (a -> a) -> a"
      "fix f = f (fix f)"
      )
"Had the value-level recursion been unavailable, we still could have
safely defined the polymorphic fix-point combinator in Haskell.  In
fact, in five different ways, never resorting to unsafe operations.
Iso-recursive data types are a well-known way to " (code "fix") ".
Using type classes or families seems less known. The
lazy " (code "ST") " approach may seem most puzzling, as the reading
of a reference cell appears to occur in pure code."
    (p
"Uncharitably speaking, Haskell, taken as a logic, is inconsistent in
more than two ways.")
    )
  (version "1.0, May 2010")
  (references
    (p
      (fileref "Fix.hs"
	"The complete Haskell code and the tests"))
    (p
      (a (@ (href "../Computation/fixed-point-combinators.html#Self-"))
	"All the ways to express the polymorphic fixpoint operator in OCaml"))
    )
)




(Description-unit "some-impredicativity"
  ("Impredicativity and explicit type applications")
  (body
    (p "On a simple example we demonstrate that the type system of
Haskell with the common rank-2 extension (not counting the extensions
in GHC 6.6) is already impredicative, and it permits explicit type,
i.e., big-lambda and type applications. This note is based on a
message by Shin-Cheng Mu from Feb 2005, and comments by Simon
Peyton-Jones and Greg Morrisett. We add the observation that big
lambda and type applications are in fact present in Haskell and can be
explicitly used by programmers.")
   (p "Polymorphic types in Haskell can only be instantiated with monomorphic
types. In other words, a type variable ranges over ground types, which do
not (overtly -- see below) contain quantified type variables. In particular, in
the following polymorphic type definition (of Church numerals)")
    (verbatim
      "type M = forall a . (a -> a) -> a -> a")
"the type variable " (code "a") " cannot be instantiated with the type
"(code "M") " itself. This so-called predicativity prevents defining
a type implicitly in terms of itself.  This property significantly
simplifies type inference; otherwise, unification, typically used to
solve type equations, becomes higher-order, which is in general
undecidable. The restriction that polytypes can only be instantiated
with monotypes is responsible for the rejection of intuitively correct
programs and seemingly makes Haskell unable to faithfully reproduce
second-order lambda calculus. Shin-Cheng Mu showed the simple example
of that, arithmetic of Church numerals:"

    (verbatim
      "zero :: M;       zero = \\f a ->  a"
      "succ :: M -> M;  succ n = \\f a -> f (n f a)"
      ""
      "add, mul :: M -> M -> M"
      "add m n = \\f a -> m f (n f a)"
      "mul m n = \\f a -> m (n f) a"
      "exp, exp2 :: M -> M -> M"
      "exp m n = n (mul m) one"
      "exp2 m n = n m"
      )

    "This program typechecks -- with the sole exception of "(code "exp")
". This may seem surprising as the equivalent " (code "exp2") " is
accepted by the typechecker. Shin-Cheng Mu pointed out that if we
write " (code "exp") " and " (code "exp2") " with the explicit big 
lambda (denoted " (code "?x -> term") ") and type application (to be denoted
" (code "term[type]") ")"

    (verbatim
      "exp  (m::M) (n::M) = n [M] ((mul m)::M->M) (one::M)"
      "exp2 (m::M) (n::M) = ?b -> \\(f::(b->b)) -> n[b->b] (m[b]) f"
      )

    "then we observe that " (code "exp") " instantiates the polymorphic
term " (code "n") " with the polymorphic type " (code "M") " -- which
is prohibited in Haskell. Hence the typechecker complains, with a
rather uninformative message ``Inferred type is less polymorphic than
expected. Quantified type variable `a' escapes.'' The term " (code
"exp2") " is accepted since the argument " (code "b") " of the 
type-lambda is assumed monotype."
    (p "The above notation for explicit type-level abstractions and
applications is not Haskell. Or is it? It turns out, the introduction
and elimination of big lambda is already part of Haskell. We can use
them to guide the typechecker when instantiating polytypes with
polytypes -- which is too effectively possible. Our guidance makes the
inference decidable. "
     "As Greg Morrisett pointed out on the discussion thread,
Haskell is impredicative: ``You can instantiate a type variable with a
" (code "newtype") " that " (em "contains") " a polymorphic type...
GHC enforces a sub-kind constraint on variables that precludes them
from ranging over types whose top-most constructor is a 
forall (and has a few more structural constraints.)  The distinction is subtle,
but important.  A predicative version of Haskell would have a much,
much simpler denotational semantics, but also prevent a number of
things that are useful and interesting.'' Indeed, we can write
" (code "exp") " after all:")

    (verbatim
      "newtype N = N{un:: forall a . (a -> a) -> a -> a}"
      ""
      "zero :: N;   zero = N ( \\f a ->  a )"
      "succ :: N -> N;  succ n = N ( \\f a -> f (un n f a) )"
      ""
      "exp, exp2 :: N -> N -> N"
      "exp m n = un n (mul m) one"
      "exp2 m n = N (\\f a -> un n (un m) f a)"
      )

"We should compare " (code "exp") " and " (code "exp2") " code here
with the explicit type lambda code above. Where we had " (code
"?t") " we have N, and where we had " (code "term[t]") " before we have 
" (code "un term") " now. Thus " (code "N") " and " (code "un") " act
as -- mark the places of -- big lambda introduction and
elimination. The notation this time is Haskell.  Wrapping polymorphic
types in newtype such as " (code "N") " also permits easy, nominal rather than
structural, equality of polymorphic types."

    (p "In this code, one may not replace " (code "N (...)") " with
"(code "N $ (...)") ".  This is yet another case where " (code "($)")
" is not the same as application with a lower precedence.")
  )
  (version "1.1, Feb 1, 2005")
  (references
    (p "Shin-Cheng Mu. "
      (Cite "Re: Polymorphic types without type constructors?")
      " A message that started the discussion, posted on the Haskell
mailing list on Tue Feb 1 22:36:00 EST 2005")
; http://www.haskell.org/pipermail/haskell/2005-February/015283.html
    (p
      (fileref "numerals-second-order.hs"
	"The complete code of the example, which compiles with Hugs,"
	"GHC 6.6. and pre-GHC 6.6."
	(br)
	"The code was originally posted on the above discussion thread "
	"on Tue Feb 1 22:36:00 EST 2005"
	))
  (p
    "Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and "
    "Mark Shields: Practical type inference for arbitrary-rank types. "
    "To appear in the Journal of Functional Programming."
    (URL "http://research.microsoft.com/Users/simonpj/papers/higher-rank/index.htm"))
  (p "Didier Le Botlan, Didier Remy: "
    "Raising ML to the Power of System F. ICFP 2003."
    (URL "http://citeseer.ist.psu.edu/lebotlan03raising.html"))
  ))


(Description-unit "computable-types"
  ("Applications of computable types")
  (body
    (p
  "We have previously introduced a functional language for computing
types and implemented it with Haskell type classes. The implementation
is trivial because it relies on the type checker to do all the
work. We now demonstrate the applications of computable types, to
ascribe signatures to terms and to drive the selection of overloaded
functions.  We can compute the type of a tree of the
depth " (code "fib(N)") " or a complex XML type, and instantiate the
" (code "read") " function to read the trees of only that shape.")
    (p 
 "We have implemented Cardelli's example, the type function " (code
"Prop") " where " (code "Prop(n)") " is the type of n-ary
propositions. For example, " (code "Prop(3)") " is the type " (code
"Bool -> Bool -> Bool -> Bool") ".  By composing the type functions
" (code "Prop") " and " (code "Fib") " we obtain the type
function "(code "StrangeProp") " of the kind " (code "NAT ->
Type") ": " (code
"StrangeProp(n)") " is the type of propositions of arity " (code "m")
", where " (code "m") " is " (code "fib(n)") ".  We use not only 
" (code "(a->)") " but
also " (code "(->a)") " as unary type functions. The former is just
" (code "(->) a") ". The latter is considered impossible.  In our
approach, " (code "(->a)") " is written almost literally as " (code
"(flip (->) a)") ".")
    (p
      "We demonstrate two different ways of defining type-level
abstractions: as `lambda-terms' in our type-level calculus (i.e., types of
the form "(code "(F t)") ") and as polymorphic types, Haskell's native type
abstractions. The two ways are profoundly related, by the correspondence
between type abstraction/instantiation and functional abstraction/application.")
    )
  (version "1.1, Sep 14, 2006")
  (references
   (p
     (fileref "TypeFN.lhs"
       "The literate Haskell code of type functions and their applications" (br)
       "It was posted as " 
       (Cite "On computable types. II. Flipping the arrow") 
       " on the Haskell mailing list on Thu, 14 Sep 2006 19:37:19
-0700 (PDT)."))
   (p
     (fileref "TypeLC.lhs"
       "Lambda-calculator on types: writing and evaluating type-level
functions" (br)
  "A type-level functional language with the notation that resembles
lambda-calculus with case distinction, fixpoint recursion, etc. Modulo
a bit of syntactic tart, the language of the type functions even looks
almost like the pure Haskell."))
   (p "Luca Cardelli: Phase Distinctions in Type Theory." (br)
     "Unpublished manuscript, 1988."
     (URL "http://lucacardelli.name/Papers/PhaseDistinctions.pdf"))
   (p "Simon Peyton Jones and Erik Meijer: "
     "Henk: A Typed Intermediate Language."
     (URL "http://www.research.microsoft.com/~simonpj/Papers/henk.ps.gz"))
  ))



(Description-unit "translucent-functor"
  ("Translucent applicative functors")
  (body
    (p
 "ML is known for its sophisticated, higher-order module system, which
is formalized in Dreyer-Crary-Harper language. Chung-chieh Shan showed
a complete translation of that language into System F-omega,
concluding that languages based on F-omega, such as Haskell with
common extensions, already support higher-order modular
programming. His paper showed a sample Haskell translation of
the most complex and interesting ML module expression: a translucent
applicative functor. Different instantiations of the functor with
respect to type-compatible arguments are type-compatible; and yet the
functor hides the representation details behind the
abstraction barrier.")
    (p
 "Dreyer-Crary-Harper language and System F-omega are deliberately
syntactically starved, to simplify formal analyses. Therefore, using
the results of Chung-chieh Shan's paper literally may be slightly
cumbersome. We attempt to interpret some of Chung-chieh Shan's results
in idiomatic Haskell, with the full use of type classes. We also
show that type sharing constraints can be expressed in a scalable
manner, so that the whole translation is practically usable.")
    (p
 "Thus we demonstrate that Haskell already has a higher-order module
language. No new extensions are required; furthermore, we avoid even
undecidable let alone overlapping instances.")
    (p
 "In the process of translating OCaml module expressions into Haskell,
we have noted several guidelines:")
    (ul
      (li "ML signatures correspond to Haskell type classes, and their
  implementations to the instances;")
      (li "Abstract types in ML correspond to either uninstantiated or
  explicitly quantified type variables in Haskell;")
      (li
	"Type sharing is expressed via type variable name sharing;")
      (li
	"Functor signatures and functors correspond to Haskell class
  declarations and class instances, resp., with type class constraints;")
      (li
	"Functor applications correspond to instance selections;")
      (li
	"OCaml signature ascription operation -- casting the module into 
  a desired signature and hiding the extras -- sometimes involves
  newtype-style tagging (which has no run-time effect);")
      (li
	"Hiding of information (`sealing', in ML-speak) is done by
  existential quantification. To gain applicativity, we quantify over
  a higher-ranked type variable: Skolem function proper.")
      )
 "In our experience these guidelines are also useful when translating from
Haskell to OCaml."
    )
  (references
   (p
     (fileref "TranslucentAppFunctor.lhs"
       "The article with the juxtaposed literate Haskell and OCaml code" (br)
       "It was posted as " 
       (Cite "Applicative translucent functors in Haskell") 
       " on the Haskell mailing list on Fri, 27 Aug 2004 16:51:43
-0700 (PDT)."))
    (p
      "Chung-chieh Shan. Higher-order modules in System F-omega and Haskell"
      (URL "http://www.cs.rutgers.edu/~ccshan/xlate/xlate.pdf"))
   (p
     "Stefan Wehr and Manuel M. T. Chakravarty. "
     "ML Modules and Haskell Type Classes: A Constructive Comparison" (br)
     "Proc. Sixth Asian Symposium on Programming Languages and Systems.
     LNCS 5356, Springer, 2008."
(URL "http://www.informatik.uni-freiburg.de/~wehr/publications/WehrChakravarty2008.html"))
 ))


(Description-unit "fibration"
  ("ML-style modules with type sharing by name")
  (body
    (p
    "When discussing higher-order module systems and their possible
implementations in Haskell, Simon Peyton-Jones noted: ``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.'' Proponents of ML-style module systems indeed emphasize the
advantage of `sharing by specification' (or `fibration') over `sharing
by construction' (or `parameterization'). Sharing by specification
gives type-equality constraints by name, whereas sharing by
construction gives type-equality constraints by position. Harper and
Pierce give examples of modular programming where the latter approach
leads to an exponential number of parameters.  It has been often
suggested that records at the type level be introduced to address this
issue.")
    (p
 "In the joint article with Chung-chieh Shan, we 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. 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.")
    )
  (references
    (fileref "Fibration.lhs"
       "The article with the juxtaposed literate Haskell and OCaml code" (br)
       "It was posted by Chung-chieh Shan on the discussion thread " 
       (Cite "Applicative translucent functors in Haskell") 
       " on the Haskell mailing list on Mon Sep 13 15:20:33 EDT 2004.")
))


(Description-unit "unsound-typeable"
  ("Typeable makes Haskell98 unsound")
  (body
    (p
      "The class Typeable provides run-time representation of types and a
type-safe cast operation. According to the documentation, 
``To this end, an unsafe cast is guarded by a test for type (representation) 
equivalence.'' Alas, that test is trivial to fake, which gives us the
" (em "total") " function of the inferred type " (code "a->b")
". This unsound cast can indeed lead to the Segmentation
fault.")

    (verbatim
      "module C where"
      ""
      "import Data.Typeable"
      "import Data.Maybe"
      ""
      "newtype W a = W{unW :: a}"
      "instance Typeable (W a) where typeOf _ = typeOf ()"
      ""
      "bad_cast x = unW . fromJust . cast $ W x"
      "-- inferred type: bad_cast :: a -> b"
      ""
      "test1 = bad_cast True ++ \"\""
      )
"When we load the above Haskell98 code in GHCi and try to evaluate
" (code "test1") " (which casts a boolean to a string), we see:"
    (verbatim
      "$ ghci /tmp/c.hs "
      "Loading package base ... linking ... done."
      "[1 of 1] Compiling C                ( /tmp/c.hs, interpreted )"
      "Ok, modules loaded: C."
      "*C> test1"
      "segmentation fault: 11"
      ))
  (version "1.1, Jul 31, 2007")
)



(Description-unit "state-algebra"
  "State Monad as a term algebra"
  (body
    (p
      "We show the implementation of the State monad as a term
algebra. We represent monadic computation by a term built from the
following constructors:")
    (verbatim
      "data Bind t f   = Bind t f"
      "data Return v   = Return v"
      "data Get        = Get"
      "data Put v      = Put v"
      )
"For example, the term "
    (code "Get `Bind` (\\v -> Put (not v) `Bind` (\\() -> Return v))")
" denotes the action of negating the current state and returning
the original state."

    (verbatim
      "runst :: RunState t s a => t -> s -> (s, a)"
      )
"The function " (code "runst") " is the observer of our
terms, or the interpreter of monadic actions. Given the term " (code
"t") " and the initial state of the type " (code "s") ", the function
interprets "(code "Get") ", " (code "Bind") ", etc. actions and
returns the final state and the resulting value. The type of the
result, " (code "a") ", is uniquely determined by the term and the state.  The
only non-trivial part is the interpretation of " (code "Bind") ", due to the
polymorphism of the monadic bind operation. We use an auxiliary class
" (code "RunBind") " for that purpose."

    (p "For completeness, we show that our term representation of
state monadic actions is an instance of " (code "MonadState")
". We can then use the familiar notation to write our sample term
above:
" (code "do{v <- get; put (not v); return v}"))

    (p "Our implementation " (em "statically") " guarantees that only
well-formed and well-typed terms  can be evaluated.")
    )
  (version "1.1, Jan 4, 2005")
  (references
    (fileref "StateAlgebra.hs"
	"The commented Haskell source code and a few tests"
	(br)
	"The code was originally posted as "
	(Cite "Initial (term) algebra for a state monad")
	" on the Haskell-Cafe mailing list on "
	"Tue, 4 Jan 2005 00:08:04 -0800 (PST)"
	)
    ))
; http://www.haskell.org/pipermail/haskell-cafe/2005-January/008241.html



   ;(br (n_))
   ;(hr)

   (footer)


)))

;(pp Content)

;========================================================================
;			HTML generation
; IMPORT
; SXML-to-HTML-ext.scm and all of its imports


; Generating HTML

(define (generate-HTML Content)
 (SRV:send-reply
  (pre-post-order Content
   (generic-web-rules Content '()))))

(generate-HTML Content)