(* Understanding Canonical Structures: usable implementation and examples
See canonical_leadup.ml for the discussions and explanations.
Canonical Structures are described in the paper
Canonical Structures for the working Coq user
Assia Mahboubi, Enrico Tassi
DOI: 10.1007/978-3-642-39634-2_5
Here, we implement them in plain OCaml.
The benefits (besides the educational)
-- #install_printer--like facility, available to all programs
(not just the top-level), implemented as a plain self-contained
OCaml library with no compiler or other magic. In fact, this file is the
implementation. See the examples in the second half of the file.
One may likewise implement registered readers, comparison functions, etc. --
as well as something like Mathematical components (groups, semirings, etc.)
-- easily experiment with type-class/implicit resolution strategies.
Everything is `user-level', with no knowledge of (let alone changes to)
the compiler internals. Everything is above-the-board and typed:
whatever the resolution algorithm one may come up with, it would be good
(or, at least, type-preserving).
-- sample experiments: disallow overlapping and ensure at most
one resolution -- or allow it, with various backtracking strategies.
We can implement bottom-up Datalog-like evaluation (which helps ensure the
uniqueness of the resolution)
We can program local typeclasses and local instances, with closure-
or closure-less, or some other experimental semantics.
-- With MetaOCaml, one can easily shift the resolution to the code
generation stage, producing code with fully resolved overloading/found
instances. The library hence becomes a viable method of implementing
implicits.
*)
(*
#load "trep.cmo";;
*)
(* general-purpose, extensible library for type representations *)
open Trep
(* The interface of `canonical structures' *)
module type implicits = sig
type 'a dict (* The canonical structure for
the type 'a, to search for *)
exception Not_resolved
val find : 'a trep -> 'a dict (* The search function, may raise
Not_resolved *)
(* Register a structure for the type
'a, represented by 'a trep
This is like the Coq command
`Canonical Structure' *)
val register : 'a trep -> 'a dict -> unit
(* More general registration, for
a structure with parameters *)
type _ rule_body =
| Fact : 'a dict -> 'a rule_body
(* 'b is existential *)
| Arg : 'b trep * ('b dict -> 'a rule_body) -> 'a rule_body
(* An entry in the (Prolog-like) database: a fact or a rule.
It also resembles a first-class pattern
*)
type reg_entry = {pat : 'a. 'a trep -> 'a rule_body option}
val register_rule : reg_entry -> unit
end
(* One implementation of the `implicits' interface
The implementation below makes the following design choices
(each of which could be chosen differently; try it!)
- when we register a canonical structure (a parameterized structure), we
do not check if the same structure (or a more general, unifiable structure)
has already been registered. We thus open the door for `overlapping
instances', in Haskell terms. If we checked, we could have enforced the
uniqueness of the resolution.
- The search procedure implements what amounts to committed choice:
if we find a match (for a structure or its argument), we never look back.
In Prolog terms, as if our program were of the form
dict(T,R) :- !.
dict(T,R) :- T = pair(X,Y), !,
dict(X,DX), dict(Y,DY), R=make_pair_dict(DX,DY).
Thus we return the first suitable canonical structure. We could have instead
returned the most specific suitable canonical structure (as Haskell does
in case of overlapping instances), or introduced priorities.
We also could have implemented Prolog-like nondeteriministic search.
*)
module MakeResolve(S:sig type 'a dict end) :
implicits with type 'a dict = 'a S.dict = struct
include S
exception Not_resolved
type _ rule_body =
| Fact : 'a dict -> 'a rule_body
(* 'b is existential *)
| Arg : 'b trep * ('b dict -> 'a rule_body) -> 'a rule_body
(* An entry in the (Prolog-like) database: a fact or a rule.
It also resembles a first-class pattern
*)
type reg_entry =
{pat : 'a. 'a trep -> 'a rule_body option}
(* The global database *)
let registry : reg_entry list ref = ref []
(* Like Coq's `Canonical Structure' command *)
let register : type a. a trep -> a dict -> unit = fun trep dict ->
let pat : type b. b trep -> b rule_body option = fun trep' ->
match teq trep trep' with
| Some Refl -> Some (Fact dict)
| _ -> None
in
registry := {pat} :: !registry
let register_rule : reg_entry -> unit = fun pat ->
registry := pat :: !registry
(* Finally, the resolution function: database lookup *)
(* This is like the SLD resolution -- but with the committed choice and
fixed modes
*)
let rec find : type a. a trep -> a dict = fun trep ->
let rec loop : reg_entry list -> a dict = function
| [] -> raise Not_resolved
| {pat}::t ->
match pat trep with
| None -> loop t
| Some rule -> do_rule rule (* committed to it *)
and do_rule : type a. a rule_body -> a dict = function
| Fact dict -> dict
| Arg (trep,rest) -> find trep |> rest |> do_rule
in loop !registry
end
(* Examples *)
(* The familiar Show example *)
module Show = MakeResolve(struct type 'a dict = 'a -> string end)
(* Define `instances' *)
let () = Show.register Int string_of_int
let () = Show.register Bool string_of_bool
(* Generic pairs, with arbitrary components.
The syntax for registration is heavy, albeit very regular.
Perhaps PPX may help
*)
let () =
let open Show in
let pat : type b. b trep -> b rule_body option = function
| Pair (x,y) ->
Some (Arg (x, fun dx -> Arg (y, fun dy ->
Fact (fun (x,y) -> "(" ^ dx x ^ "," ^ dy y ^ ")"))))
| _ -> None
in
register_rule {pat}
(* A specific instance for bool*bool pairs *)
let () = Show.register (Pair(Bool,Bool))
(fun (x,y) -> string_of_bool x ^ string_of_bool y)
let _ = Show.find Int 1;;
(* - : string = "1" *)
let _ = Show.find (Pair (Int,Int)) (1,2)
(* - : string = "(1,2)" *)
let _ = Show.find (Pair (Int,(Pair (Int,Int)))) (10,(11,12))
(*
* - : string = "(10,(11,12))"
*)
let _ = Show.find (Pair (Int,Bool)) (1,true)
(*
* - : string = "(1,true)"
*)
let _ = Show.find (Pair (Bool,Bool)) (false,true)
(*
* - : string = "falsetrue"
*)
(* Lists are very useful *)
let () =
let open Show in
let pat : type b. b trep -> b rule_body option = function
| List x ->
Some (Arg (x, fun dx ->
Fact (fun lst -> "[" ^ String.concat ";" (List.map dx lst) ^ "]")))
| _ -> None
in
register_rule {pat}
(* User-defined data type *)
type my_fancy_datatype = Fancy of int * string * (int -> string)
(* Register with the trep library. The type has no parameters.
The name can be arbitrary. It should be unique within a module, but
does not have to be globally unique.
*)
type _ trep += MyFancy : my_fancy_datatype trep
let () =
let teq : type a b. a trep -> b trep -> (a,b) eq option = fun x y ->
match (x,y) with (MyFancy,MyFancy) -> Some Refl | _ -> None
in teq_extend {teq=teq}
let () = Show.register MyFancy (function Fancy(x,y,_) ->
string_of_int x ^ "/" ^ y ^ "/" ^ "")
(* Now we can use fancy in combination with any already registered types *)
let _ = Show.find (Pair(Int,Pair(MyFancy,Bool)))
(4,(Fancy(5,"fancy",fun x -> "x"),true))
(*
* - : string = "(4,(5/fancy/,true))"
*)
let _ = Show.find (List(List(Pair(MyFancy,Int))))
[[(Fancy(1,"fanci",fun x -> "x"),5)];[]]
(*
* - : string = "[[(1/fanci/,5)];[]]"
*)
(* Well, `proof search'! *)
;;