* [Caml-list] Wanted: GADT examples: string length, counting module x
@ 2012-03-22 6:01 oleg
2012-03-22 9:04 ` Gabriel Scherer
2012-03-22 16:58 ` [Caml-list] " Goswin von Brederlow
0 siblings, 2 replies; 3+ messages in thread
From: oleg @ 2012-03-22 6:01 UTC (permalink / raw)
To: goswin-v-b; +Cc: caml-list
Somehow typed tagless interpreters (embeddings of a typed language)
and length-parameterized lists with the append function are the most
popular examples of GADTs. Neither of them seem to be particularly
good or compelling examples. One can write typed interpreters in the
final-tagless style, with no GADTs. Writing append function whose type
says the length of the resulting list is the sum of the lengths of the
argument lists is cute. However, this example does not go too far, as
one discovers when trying to write List.filter for
length-parameterized lists.
The ML2010 talk on GADT emulation specifically used a different
illustrating example: a sort of generic programming, or implementing
N-morphic functions:
http://okmij.org/ftp/ML/first-class-modules/first-class-modules-talk-notes.pdf
Polymorphic functions must operate uniformly on their arguments, which
means they can't use a specific efficient operation if the argument
happens to be of a convenient type (like int of float
array). N-morphic functions can take such an advantage.
The running example of the talk combined value and the shape
information in the same data type:
type 'a sif = Int of (int,'a) eq * int
| Flo of (float,'a) eq * float
val add_sif : 'a sif -> 'a sif -> 'a sif
Shape may well be separated from the value:
type 'a shape = Int of (int,'a) eq
| Flo of (float,'a) eq
val add_sif : 'a shape -> 'a -> 'a -> 'a
and so we pass values to add_sif without `boxing' and wrapping.
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: [Caml-list] Wanted: GADT examples: string length, counting module x
2012-03-22 6:01 [Caml-list] Wanted: GADT examples: string length, counting module x oleg
@ 2012-03-22 9:04 ` Gabriel Scherer
2012-03-22 16:58 ` [Caml-list] " Goswin von Brederlow
1 sibling, 0 replies; 3+ messages in thread
From: Gabriel Scherer @ 2012-03-22 9:04 UTC (permalink / raw)
To: oleg; +Cc: goswin-v-b, caml-list
In this example, you use GADTs to safely provide runtime type
information on untagged data. This can also be seen as a specific case
of the "runtime type information" promoted by Alain Frisch [1] or
equivalently as a dual (in the sum-of-data vs. product-of-functions
sense) of type-classes, where you have a predicate over a subset of
the types ("sif" being read as an "is_a_number" type constraint) whose
instances are closed / fixed at class definition time, to which
operations can be added modularly: `add` now, `mult` later. This can
then be related to Pottier and Gauthier's "concretization" of
type-classes mentioned in my previous message.
[1] http://www.lexifi.com/blog/dynamic-types
[2] http://gallium.inria.fr/~fpottier/publis/fpottier-gauthier-hosc.pdf
> One can write typed interpreters in the
> final-tagless style, with no GADTs.
Isn't this true of all GADTs examples? You have already shown that
GADTs can be relatively-practically expressible with equality types. I
suspect the justification for GADTs is not increased expressivity, but
a simpler/more familiar way to implement those
type-information-passing techniques -- just as ordinary algebraic
datatypes could be expressed with functional encodings, but are more
practical and convenient to use in the usual case. Besides, there is
the down-to-earth efficiency benefit of directly using first-order
data instead of functional encodings.
On Thu, Mar 22, 2012 at 7:01 AM, <oleg@okmij.org> wrote:
>
> Somehow typed tagless interpreters (embeddings of a typed language)
> and length-parameterized lists with the append function are the most
> popular examples of GADTs. Neither of them seem to be particularly
> good or compelling examples. One can write typed interpreters in the
> final-tagless style, with no GADTs. Writing append function whose type
> says the length of the resulting list is the sum of the lengths of the
> argument lists is cute. However, this example does not go too far, as
> one discovers when trying to write List.filter for
> length-parameterized lists.
>
> The ML2010 talk on GADT emulation specifically used a different
> illustrating example: a sort of generic programming, or implementing
> N-morphic functions:
> http://okmij.org/ftp/ML/first-class-modules/first-class-modules-talk-notes.pdf
>
> Polymorphic functions must operate uniformly on their arguments, which
> means they can't use a specific efficient operation if the argument
> happens to be of a convenient type (like int of float
> array). N-morphic functions can take such an advantage.
>
> The running example of the talk combined value and the shape
> information in the same data type:
>
> type 'a sif = Int of (int,'a) eq * int
> | Flo of (float,'a) eq * float
>
> val add_sif : 'a sif -> 'a sif -> 'a sif
>
> Shape may well be separated from the value:
>
> type 'a shape = Int of (int,'a) eq
> | Flo of (float,'a) eq
>
> val add_sif : 'a shape -> 'a -> 'a -> 'a
>
> and so we pass values to add_sif without `boxing' and wrapping.
>
>
>
>
>
>
> --
> Caml-list mailing list. Subscription management and archives:
> https://sympa-roc.inria.fr/wws/info/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
^ permalink raw reply [flat|nested] 3+ messages in thread
* [Caml-list] Re: Wanted: GADT examples: string length, counting module x
2012-03-22 6:01 [Caml-list] Wanted: GADT examples: string length, counting module x oleg
2012-03-22 9:04 ` Gabriel Scherer
@ 2012-03-22 16:58 ` Goswin von Brederlow
1 sibling, 0 replies; 3+ messages in thread
From: Goswin von Brederlow @ 2012-03-22 16:58 UTC (permalink / raw)
To: oleg; +Cc: goswin-v-b, caml-list
oleg@okmij.org writes:
> Somehow typed tagless interpreters (embeddings of a typed language)
> and length-parameterized lists with the append function are the most
> popular examples of GADTs. Neither of them seem to be particularly
> good or compelling examples. One can write typed interpreters in the
> final-tagless style, with no GADTs. Writing append function whose type
> says the length of the resulting list is the sum of the lengths of the
> argument lists is cute. However, this example does not go too far, as
> one discovers when trying to write List.filter for
> length-parameterized lists.
>
> The ML2010 talk on GADT emulation specifically used a different
> illustrating example: a sort of generic programming, or implementing
> N-morphic functions:
> http://okmij.org/ftp/ML/first-class-modules/first-class-modules-talk-notes.pdf
An interesting talk to read. But unless I'm mistaken that isn't using
ocamls new GADT types but implements it own.
MfG
Goswin
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2012-03-22 16:58 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2012-03-22 6:01 [Caml-list] Wanted: GADT examples: string length, counting module x oleg
2012-03-22 9:04 ` Gabriel Scherer
2012-03-22 16:58 ` [Caml-list] " Goswin von Brederlow
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).