(* Understanding Canonical Structures: lead-up
Canonical Structures for the working Coq user
Assia Mahboubi, Enrico Tassi
DOI: 10.1007/978-3-642-39634-2_5
We render the examples in OCaml, making very explicit the connections with
Prolog (Horn clause resolution).
We changed the running example, from Eq class to Show class, for ease
of explaining.
*)
(*
#load "trep.cmo";;
*)
(* Define the abbrevation for the overloaded function whose instance we are
searching for.
In the Canonical Structures paper, the 'a show_dict below is called `class'.
`Dictionary' seems a more familiar name for it.
For technical reasons, Coq wraps this function into a one-field record.
There is no need for it in OCaml.
*)
type 'a show_dict = 'a -> string
(* trep describes our universe of types *)
open Trep
(* Suppose that we have find_show .... Then we can write the example
let ex = (find_show Int) 1
as shown below.
Like in Coq, we need 'a trep, a term that witnesses a type
(in the example above, the type of the literal 1).
The type checker easily figures out that 'a is int.
The type checker can easily synthesise the trep value Int (the witness).
But the type checker can't do the job of find_show, to find
a particular record of the type int show_dict.
Finding such a record amounts to proof search, as the Canonical Structures
paper explained.
*)
module Ex1(S:sig val find_show : 'a trep -> 'a show_dict end) = struct
open S
let ex = (find_show Int) 1
(* In fact, we can define the `generic function' *)
let show trep x = find_show trep x
(* val show : 'a trep -> 'a -> string *)
(* Although 'a trep looks like a `dictionary' in the standard
implementation of type-classes, it is not.
'a trep is a term representation of the type 'a, essentially a hash
value, independent of show, read or any other operation.
It is present in the Coq code
Once can easily imagine in the near future OCaml compiler automatically
synthesizes 'a trep value, e.g., as a `hash' of the internal type
represnetation in the OCaml compiler.
*)
let ex' = show Int 4
end
(* How can we actually implement find_show? *)
(* By searching a global database: a registry. This is the approach
of Canonical structures.
*)
(* First attempt *)
module RegistryShow1 = struct
(* An association of a type (rep) and the dictionary. The type variable 'a
below is abstracted over (existentialized)
*)
type show_reg_entry =
Showable : 'a trep * 'a show_dict -> show_reg_entry
(* The global database *)
let show_registry : show_reg_entry list ref = ref []
(* Register a canonical structure in the database. This is like the Coq
command `Canonical Structure'
For simplicity, we just add a new association of the type t and
the t show_dict to the registry. We should have checked if the registry
already had an association for that type t -- and raise an error.
That check will ensure that there is at most one t show_dict
for each type t: uniqueness makes the resolution predictable.
OTH, we could have allowed duplicates, and make the resolution algorithm
nondeteriministic.
*)
let show_register : 'a trep -> 'a show_dict -> unit = fun trep dict ->
show_registry := Showable (trep,dict) :: !show_registry
(* Finally, the resolution function: the database lookup *)
let find_show : type a. a trep -> a show_dict = fun trep ->
let rec loop : show_reg_entry list -> a show_dict = function
| [] -> failwith "find_show: resolution failed"
| Showable(trep',dict)::t -> match teq trep trep' with
| Some Refl -> dict
| _ -> loop t
in loop !show_registry
end
(* Register the show of integers *)
let () = RegistryShow1.show_register Int string_of_int
let _ = let module M = Ex1(RegistryShow1) in (M.ex, M.ex')
(* - : string * string = ("1", "4")
*)
(* Let's review what we have done. We have a database of facts, like the
following:
showable(int,int_show_dict).
...
and we search it, with the query like ?- showable(int,X).
returning the first found answer.
Looks familiar?
*)
(*
Besides facts, Prolog/Datalog also has rules. Consider pairs:
The ('a * 'b) dictionary now has parameters.
*)
let make_pair_dict : 'a show_dict * 'b show_dict -> ('a * 'b) show_dict =
fun (dx,dy) -> fun (x,y) -> "(" ^ dx x ^ "," ^ dy y ^ ")"
(*
In other words, we can show pairs _provided_ we can show their components.
Resolution becomes conditional, and recursive. Thus our database should
have something like
showable(pair(X,Y),R) :-
showable(X,DX), showable(Y,DY), R=make_pair_dict(DX,DY).
*)
module RegistryShow2 = struct
(* An entry in the database: a fact or a rule.
It also resembles a first-class pattern
*)
type show_reg_entry =
| Fact : 'a trep * 'a show_dict -> show_reg_entry (* as before *)
| Rule : {pat : 'a. 'a trep -> 'a show_dict option} -> show_reg_entry
(* The global database *)
let show_registry : show_reg_entry list ref = ref []
(* Register a canonical structure in the database. This is like the Coq
command `Canonical Structure'
*)
let show_register : type a. a trep -> a show_dict -> unit = fun trep dict ->
show_registry := Fact (trep,dict) :: !show_registry
let show_register' : show_reg_entry -> unit = fun entry ->
show_registry := entry :: !show_registry
(* Finally, the resolution function: database lookup *)
(* This is SLD resolution! But with committed choice and with fixed modes. *)
let find_show : type a. a trep -> a show_dict = fun trep ->
let rec loop : show_reg_entry list -> a show_dict = function
| [] -> failwith "find_show: resolution failed"
| Fact (trep',dict)::t -> begin match teq trep trep' with
| Some Refl -> dict
| None -> loop t
end
(* Committed choice: If the rule's head matches,
we are committed to it. That is, we don't permit backtracking here.
Neither do Canonical Structures of Coq.
That is, we implement something like
showable(T,R) :- T = pair(X,Y), !,
showable(X,DX), showable(Y,DY), R=make_pair_dict(DX,DY).
There isn't anything in principle that stops us from supporting
backtracking though.
*)
| Rule {pat}::t -> match pat trep with
| Some dict -> dict
| None -> loop t
in loop !show_registry
end
(* Register the old int_show_dict *)
let () = RegistryShow2.show_register Int string_of_int
(* Register the pairs *)
let () = let open RegistryShow2 in
let pat : type b. b trep -> b show_dict option = function
| Pair (x,y) -> Some (make_pair_dict (find_show x, find_show y))
| _ -> None
in
show_register' @@ Rule {pat}
(* We can use staging to inline string_of_int etc *)
let _ = let module M = Ex1(RegistryShow2) in (M.ex, M.ex')
module Ex2(S:sig val find_show : 'a trep -> 'a show_dict end) = struct
open S
let show trep x = find_show trep x
let ex = show (Pair (Int,Int)) (1,2)
let ex' = show (Pair (Int,(Pair (Int,Int)))) (10,(11,12))
end
let _ = let module M = Ex2(RegistryShow2) in (M.ex, M.ex')
(* - : string * string = ("(1,2)", "(10,(11,12))") v*)
(* I can use this already for lift in MetaOCaml! *)
;;