add advanced examples

git-svn-id: http://caml.inria.fr/svn/ocamldoc/trunk@12322 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

manual/manual/refman/exten.etex

@@ -1061,14 +1061,64 @@ exhaustive (the "Add" case cannot happen).
           | App(_,_) -> 0
 \end{verbatim}
 
-% Another frequent application of GADTs is equality witnesses.
+\paragraph{Advanced examples}
-% \begin{verbatim}
+The "term" type we have defined above is an {\em indexed} type, where
-%         type (_,_) eq = Eq : ('a,'a) eq
+a type parameter reflects the value contents.
+Another use of GADTs is {\em singleton} types, where a GADT value
+represents exactly one type. This value can be used as runtime
+representation for this type, and a function receiving it can have a
+polytypic behavior.
 
-%         let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x
+Here is an example of a polymorphic function that takes the
-%         val cast : ('a, 'b) eq -> 'a -> 'b = <fun>
+runtime representation of some type "t" and a value of the same type,
-% \end{verbatim}
+then pretty-print the value as a string:
-% Here type "eq" has only one constructor, and by matching on it one
+\begin{verbatim}
-% adds a local constraint allowing the conversion between "a" and "b".
+        type _ typ =
-% By building such equality witnesses, one can make equal types which
+          | Int : int typ
-% are syntactically different.
+          | String : string typ
+          | Pair : 'a typ * 'b typ -> ('a * 'b) typ
+
+        let rec to_string: type t. t typ -> t -> string =
+          fun t x ->
+          match t with
+          | Int -> string_of_int x
+          | String -> Printf.sprintf "%S" x
+          | Pair(t1,t2) ->
+              let (x1, x2) = x in
+              Printf.sprintf "(%s,%s)" (to_string t1 x1) (to_string t2 x2)
+\end{verbatim}
+
+Another frequent application of GADTs is equality witnesses.
+\begin{verbatim}
+        type (_,_) eq = Eq : ('a,'a) eq
+
+        let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x
+\end{verbatim}
+Here type "eq" has only one constructor, and by matching on it one
+adds a local constraint allowing the conversion between "a" and "b".
+By building such equality witnesses, one can make equal types which
+are syntactically different.
+
+Here is an example using both singleton types and equality witnesses
+to implement dynamic types.
+\begin{verbatim}
+        let rec eq_type : type a b. a typ -> b typ -> (a,b) eq option =
+          fun a b ->
+          match a, b with
+          | Int, Int -> Some Eq
+          | String, String -> Some Eq
+          | Pair(a1,a2), Pair(b1,b2) ->
+            begin match eq_type a1 b1, eq_type a2 b2 with
+            | Some Eq, Some Eq -> Some Eq
+            | _ -> None
+            end
+          | _ -> None
+
+        type dyn = Dyn : 'a typ * 'a -> dyn
+
+        let get_dyn : type a. a typ -> dyn -> a option =
+          fun a (Dyn(b,x)) ->
+          match eq_type a b with
+            None -> None
+          | Some Eq -> Some x
+\end{verbatim}