(* 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";;
*)
(* In the Canonical Structures paper, the 'a show_dict below is called `class'.
`Dictionary' seems a more familiar name for it.
Why we need a record? It would be clear later
*)
type 'a show_dict = {show : '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).show 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).show 1
(* In fact, we can define the `generic function' *)
let show trep x = (find_show trep).show 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
(* Sample show dictionary *)
let int_show_dict : int show_dict = {show = string_of_int }
(* and register it *)
let () = RegistryShow1.show_register Int int_show_dict
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 pair_show_dict : 'a show_dict * 'b show_dict -> ('a * 'b) show_dict =
fun (dx,dy) ->
{show = fun (x,y) -> "(" ^ dx.show x ^ "," ^ dy.show 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).
*)
(* Now, we have parameters, which are to be searched for. So,
find_show is to be invoked recursively *)
type _ show_rule_body =
| Fact : 'a show_dict -> 'a show_rule_body
(* 'b is existential *)
| Arg : 'b trep * ('b show_dict -> 'a show_rule_body) -> 'a show_rule_body
module RegistryShow2 = struct
(* An entry in the database: a fact or a rule.
It also resembles a first-class pattern
*)
type show_reg_entry =
{pat : 'a. 'a trep -> 'a show_rule_body option}
(* 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 ->
let pat : type b. b trep -> b show_rule_body option = fun trep' ->
match teq trep trep' with
| Some Refl -> Some (Fact dict)
| _ -> None
in
show_registry := {pat} :: !show_registry
let show_register' : show_reg_entry -> unit = fun pat ->
show_registry := pat :: !show_registry
(* Finally, the resolution function: database lookup *)
(* This is SLD resolution! But with committed choice and with fixed modes. *)
let rec 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"
(* Committed choice: If the rule's head matches,
we are committed to it. That is, we don't permit overlapping here.
Neither do Canonical Structures of Coq.
There isn't anything in principle that stops us from supporting
overlapping: we need to change the type of the SRule so that
errors in finding 'b trep and constructing the dictionary
could be caught and we backtrack, that is, recur to loop
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).
*)
| {pat}::t ->
match pat trep with
| None -> loop t
| Some rule -> do_rule rule
and do_rule : type a. a show_rule_body -> a show_dict = function
| Fact dict -> dict
| Arg (trep,rest) -> find_show trep |> rest |> do_rule
in loop !show_registry
end
(*
let show_register1 : type a. a trep -> a show_dict -> unit = fun trep dictf ->
let pat : type b. b trep -> b show_rule_body option = function
| List x -> Some (Arg (x, fun d -> Fact (dictf d)))
| _ -> None
in
show_registry := {pat} :: !show_registry
*)
(* Register the old int_show_dict *)
let () = RegistryShow2.show_register Int int_show_dict
(* Register the pairs *)
let () =
let pat : type b. b trep -> b show_rule_body option = function
| Pair (x,y) ->
Some (Arg (x, fun dx -> Arg (y, fun dy ->
Fact (pair_show_dict (dx,dy)))))
| _ -> None
in
RegistryShow2.show_register' {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).show 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! *)
;;