Version française
Home     About     Download     Resources     Contact us    
Browse thread
Relating parts of ML and Haskell
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Jacques Carette <carette@m...>
Subject: Relating parts of ML and Haskell
[I am posting this message to caml-list on behalf of Oleg, who is 
not a subscriber.  I asked him to compose this, as the messages he 
points to are just as relevant to Caml programmers as to Haskell 
programmers to understand 'the other side' -- Jacques]

Correspondence between ML structures and functors and Haskell type
classes is described in a message:

Applicative translucent functors in Haskell
http://www.haskell.org/pipermail/haskell/2004-August/014463.html

The message is based on a draft paper by Chung-chieh Shan, who showed
the complete translation of Dreyer-Crary-Harper module language into
System Fw. The message attempted to interpret some of Shan's results
in idiomatic Haskell with the full use of type classes. That message
is both Haskell and OCaml literate code. It can be loaded in GHCi or
Hugs -98, and (after some sed filtering) into OCaml.

The upshot of the correspondence between type classes and ML modules
is as follows:

  ML signatures correspond to Haskell type classes, and their
  implementations to the instances

  Abstract types in ML correspond to either uninstantiated or
  explicitly quantified type variables in Haskell

  Type sharing is expressed via type variable name sharing

  Functor (signatures or structures) correspond to Haskell (class
  declarations or instances) with type class constraints

  The argument of functors is expressed via types, with additional labels
  when needed for finer differentiation

  Functor applications are done by instance selection based on types
  at hand plus the additional labels

  OCaml signature attribution operation -- casting the module or
  the result of the functor into a desired signature and hiding
  the extras -- sometimes involves additional tagging/untagging tricks
  (cf. SetESet). This tagging, done via newtype, is syntactic only and
  has no run-time  effect.

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


A follow-up message (written together with Chung-chieh Shan)

Applicative translucent functors in Haskell
http://www.haskell.org/pipermail/haskell/2004-September/014515.html

is devoted to the problem of sharing constraints and exponential
explosion and brittleness of ``sharing by construction'' (or
positional sharing). The message translates 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.