(* 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' *)
(* XXX Add with_local_register for emulating local registration *)
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
more flexible matching and
for rules
*)
type rule_entry = {pat: 'a. 'a trep -> 'a dict option}
val register_rule : rule_entry -> unit
end
(* If we would like to check if a pattern has matched without needing to
construct a dictionary, we could introduce a delayed application:
type 'a app = App : 'b * ('b -> 'a) -> 'a app
type rule_entry = {pat: 'a. 'a trep -> 'a dict app option}
or just
type rule_entry = {pat: 'a. 'a trep -> 'a dict Lazy.t option}
Incidentally, we can do memoization by registering the canonical value
for a concrete type.
*)
(* 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_entry = {pat: 'a. 'a trep -> 'a dict option}
(* An entry in the (Prolog-like) database: a fact or a rule.
It also resembles a first-class pattern
*)
type reg_entry = rule_entry
(* The global database *)
let registry : reg_entry list ref = ref []
let register_rule : rule_entry -> unit = fun entry ->
registry := entry :: !registry
(* Like Coq's `Canonical Structure' command *)
let register : type a. a trep -> a dict -> unit = fun trep dict ->
let pat : type a. a trep -> a dict option = fun trep' ->
match teq trep trep' with
| Some Refl -> Some dict
| _ -> None
in
register_rule {pat}
(* 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 dict -> dict (* committed to it *)
in loop !registry
end
(* Examples *)
(* The familiar Show example, also showing the type itself *)
module ShowType = MakeResolve(struct type 'a dict = string end)
module Show = MakeResolve(struct type 'a dict = 'a -> string end)
(* Define `instances' *)
let () = ShowType.register Int "Int"
let () = ShowType.register Bool "Bool"
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 ShowType in
let pat : type b. b trep -> b dict option = function
| Pair (tx,ty) -> Some ("(" ^ find tx ^ " * " ^ find ty ^ ")")
| _ -> None
in
register_rule {pat}
let () =
let open Show in
let pat : type b. b trep -> b dict option = function
| Pair (tx,ty) ->
Some (fun (x,y) -> "(" ^ find tx x ^ "," ^ find ty y ^ ")")
| _ -> None
in
register_rule {pat}
(* A specific instance for bool*bool pairs *)
let () = Show.register (Pair(Bool,Bool)) @@
let btos = function true -> "T" | false -> "F" in
fun (x,y) -> btos x ^ btos y
let _ = ShowType.find Int;;
(* - : string = "Int" *)
let _ = Show.find Int 1;;
(* - : string = "1" *)
let _ = ShowType.find (Pair (Int,Int))
(* - : string = "(Int * Int)" *)
let _ = Show.find (Pair (Int,Int)) (1,2)
(* - : string = "(1,2)" *)
let _ = ShowType.find (Pair (Int,(Pair (Int,Int))))
(* - : string = "(Int * (Int * Int))" *)
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 = "FT" *)
let _ = Show.find (Pair(Int, Pair(Bool,Bool))) (1,(false,true))
(* - : string = "(1,FT)" *)
(* Lists are very useful *)
let () =
let open Show in
let pat : type b. b trep -> b dict option = function
| List tx ->
let dx = find tx in
Some (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'! *)
(* The next example: Read
Here, the overloading is resolved on the return type
*)
module Read = MakeResolve(struct
type 'a dict = Scanf.Scanning.in_channel -> 'a end)
let () = Read.register Int (fun ch -> Scanf.bscanf ch "%d" Fun.id)
let () = Read.register Bool (fun ch -> Scanf.bscanf ch "%B" Fun.id)
let () =
let open Read in
let pat : type b. b trep -> b dict option = function
| Pair (tx,ty) ->
Some (fun ch -> Scanf.bscanf ch "(%r, %r)" (find tx) (find ty)
(fun x y -> (x,y)))
| _ -> None
in
register_rule {pat}
let _ = Read.find (Pair(Int,Pair(Bool,Bool)) )
(Scanf.Scanning.from_string "(1,(true,false))")
(* - : int * (bool * bool) = (1, (true, false)) *)
let _ = Read.find (Pair(Int,Pair(Bool,Bool)) )
(Scanf.Scanning.from_string "(1, (true, false))")
(* - : int * (bool * bool) = (1, (true, false)) *)
(* Final example: ReadShow: the combination of Read and Show.
The reason to make this combination is that we guarantee that
for the given type both reading and showing is available.
One may define show for function types (just to print ""),
but one can't define read.
Furthermore, ReadShow ensures that read and show instances are consustent:
read can parse what show can show. In Coq, this side-condition would
have been stated as a lemma to prove. In OCaml, we merely note it,
for the programmer to ensure.
Incidentally, in our earlier examples of separately defined show and read,
the coherency property was indeed violated: in the case of bool*bool pairs,
which are shown in a particular way.
The ReadShow example follows very closely the LEQ-EQ example in
Mahboubi and Tassi's paper.
Availability of both read and show lets us compose them: the composition
(show . read) may regarded as normalization: converting a printing
representation into a canonical form.
*)
type 'a readshow =
{read: 'a Read.dict; show: 'a Show.dict;
norm: string -> string (* normalization function *)
}
module ReadShow = MakeResolve(struct type 'a dict = 'a readshow end)
(* A generic instance. It checks that both read and show are available *)
let () =
let open ReadShow in
let pat : type b. b trep -> b dict option = fun t ->
let read = Read.find t and show = Show.find t in
let norm = fun x -> Scanf.Scanning.from_string x |> read |> show in
Some {read;show;norm}
in
register_rule {pat}
(* Before we have registered a specific show for bool*bool.
It is not compatible with read, so we have to define a specific
instance of ReadShow for bool*bool
*)
let () =
let open ReadShow in
let pat : type b. b trep -> b dict option = function
| Pair (tx,ty) as t ->
let read = Read.find t and
show (x,y) = "(" ^ (find tx).show x ^ "," ^ (find ty).show y ^ ")" in
let norm = fun x -> Scanf.Scanning.from_string x |> read |> show in
Some {read;show;norm}
| _ -> None
in
register_rule {pat}
let _ = (ReadShow.find (Pair(Int,Pair(Bool,Bool)))).show (1,(true,false))
(* - : string = "(1,(true,false))" *)
(* (show . read) is not a problem for us *)
let _ = (ReadShow.find (Pair(Int,Pair(Bool,Bool)))).norm
"(1, (true, false))"
(* - : string = "(1,(true,false))" *)
(* Other example to try: multiparameter type classes: resolution on
several parameters. Hint: group the parameters into a tuple, and define
type _ dict = Dict : xxx -> ('a * 'b) dict
as a GADT.
*)
;;