Add bidi_local

README.md

@@ -26,6 +26,20 @@
   Type inference and elaborator are implemented but the environment construction
   doesn't check for overlapping instances yet.
 
+- `bidi_local` attempts to implement ["Local Type Inference"][bidi_local] by
+  Piece and Turner.
+
+  This is a bidirectional type checking mechanism where we alternate between
+  checking mode (where we have type annotations available) and synthesis mode.
+
+  Thus this requires type annotations for let-functions declarations.
+
+  The type system supports subtyping (with `null`). The way it works is it
+  collects lower/upper bound constraints for type variables and then synthesises
+  the most general type for type variables at polymorphic abstraction
+  elimination.
+
+
 # Development
 
 ```
@@ -48,3 +62,4 @@ make test
 [inferno]: https://gitlab.inria.fr/fpottier/inferno/
 [THIH]: https://web.cecs.pdx.edu/~mpj/thih/thih.pdf
 [tomprimozic/type-systems]: https://github.com/tomprimozic/type-systems
+[bidi_local]: https://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf

bidi_local/bidi_local.ml

@@ -0,0 +1,69 @@
+module Expr = struct
+  include Syntax.Expr
+
+  include Nice_parser.Make (struct
+    type token = Parser.token
+
+    type result = Syntax.expr
+
+    let parse = Parser.expr_eof
+
+    let next_token = Lexer.token
+
+    exception ParseError = Parser.Error
+
+    exception LexError = Lexer.Error
+  end)
+end
+
+module Ty = struct
+  include Syntax.Ty
+
+  include Nice_parser.Make (struct
+    type token = Parser.token
+
+    type result = Syntax.ty
+
+    let parse = Parser.ty_eof
+
+    let next_token = Lexer.token
+
+    exception ParseError = Parser.Error
+
+    exception LexError = Lexer.Error
+  end)
+end
+
+module Ty_sch = struct
+  include Syntax.Ty_sch
+
+  include Nice_parser.Make (struct
+    type token = Parser.token
+
+    type result = Syntax.ty_sch
+
+    let parse = Parser.ty_sch_eof
+
+    let next_token = Lexer.token
+
+    exception ParseError = Parser.Error
+
+    exception LexError = Lexer.Error
+  end)
+end
+
+module Type_error = Type_error
+module Var = Var
+
+module Env = struct
+  include Infer.Env
+
+  let assume_val name ty env =
+    add_val ~kind:Val_top env name (Ty_sch.parse_string ty)
+end
+
+let infer = Infer.infer
+
+let enable_colors = Layout.enable_colors
+
+let () = Expr.pp_exceptions ()

bidi_local/bin/dune

@@ -0,0 +1,4 @@
+(executable
+ (public_name bidi_local)
+ (name main)
+ (libraries bidi_local base stdio unix))

bidi_local/bin/main.ml

@@ -0,0 +1,31 @@
+open Base
+open Bidi_local
+
+let () =
+  let () = if Unix.isatty Unix.stdout then enable_colors true in
+  let env =
+    Env.empty
+    |> Env.assume_val "id" "a . a -> a"
+    |> Env.assume_val "null" "a . a?"
+    |> Env.assume_val "one" "int"
+    |> Env.assume_val "succ" "int -> int"
+    |> Env.assume_val "nil" "a . list[a]"
+    |> Env.assume_val "cons" "a . (a, list[a]) -> list[a]"
+    |> Env.assume_val "map" "a, b . (a -> b, list[a]) -> list[b]"
+    |> Env.assume_val "choose" "a . (a, a) -> a"
+    |> Env.assume_val "choose3" "a . (a, a, a) -> a"
+    |> Env.assume_val "choose4" "a . (a, a, a, a) -> a"
+    |> Env.assume_val "hello" "string"
+    |> Env.assume_val "pair" "a, b . (a, b) -> pair[a, b]"
+    |> Env.assume_val "plus" "(int, int) -> int"
+    |> Env.assume_val "true" "bool"
+    |> Env.assume_val "ifnull" "a . (a?, a) -> a"
+    |> Env.assume_val "eq" "a . (a, a) -> bool"
+  in
+  let s = Stdio.In_channel.input_all Stdio.stdin in
+  let e = Expr.parse_string (String.strip s) in
+  match infer ~env e with
+  | Ok e -> Caml.Format.printf "%s@." (Expr.show e)
+  | Error err ->
+    let report = Type_error.to_report err in
+    Caml.Format.printf "%a@." Location.print_report report

bidi_local/debug.ml

@@ -0,0 +1,26 @@
+(**
+
+  Debug flags which influence the amount of logging information and pretty
+  printing.
+
+  Flags are controlled through DEBUG environment variables, use it like:
+
+    $ DEBUG=sgi dune exec -- COMMAND
+
+  The above invocation will toggle glags [s], [g] and [i] to be "on".
+
+ *)
+
+open! Base
+
+let flags = Caml.Sys.getenv_opt "DEBUG" |> Option.value ~default:""
+
+let log_solve = String.mem flags 's'
+
+let log_generalize = String.mem flags 'g'
+
+let log_instantiate = String.mem flags 'i'
+
+let log_check = String.mem flags 'c'
+
+let log_levels = String.mem flags 'l'

bidi_local/dune

@@ -0,0 +1,11 @@
+(library
+ (name bidi_local)
+ (preprocess (pps ppx_sexp_conv))
+ (libraries base pprint nice_parser)
+ )
+
+(ocamllex lexer)
+
+(menhir
+  (modules parser)
+  (flags --explain --dump))

bidi_local/import.ml

@@ -0,0 +1,108 @@
+include Base
+
+module Monad = struct
+  include Base.Monad
+
+  (** A signature for modules implementing monadic let-syntax. *)
+  module type MONAD_SYNTAX = sig
+    type 'a t
+
+    val return : 'a -> 'a t
+
+    val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+    val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+  end
+
+  (** Make a monadic syntax out of the monad. *)
+  module Make_monad_syntax (P : Base.Monad.S) :
+    MONAD_SYNTAX with type 'a t := 'a P.t = struct
+    let return = P.return
+
+    let ( let* ) v f = P.bind v ~f
+
+    let ( let+ ) v f = P.map v ~f
+  end
+
+  module type S = sig
+    include Base.Monad.S
+
+    module Monad_syntax : MONAD_SYNTAX with type 'a t := 'a t
+  end
+
+  module Make (P : Basic) : S with type 'a t := 'a P.t = struct
+    module Self = Base.Monad.Make (P)
+    include Self
+
+    module Monad_syntax = Make_monad_syntax (struct
+      type 'a t = 'a P.t
+
+      include Self
+    end)
+  end
+end
+
+module MakeId () = struct
+  let c = ref 0
+
+  let fresh () =
+    Int.incr c;
+    !c
+
+  let reset () = c := 0
+end
+
+module type SHOWABLE = sig
+  type t
+
+  val show : t -> string
+
+  val print : ?label:string -> t -> unit
+end
+
+module Showable (S : sig
+  type t
+
+  val layout : t -> PPrint.document
+end) : SHOWABLE with type t = S.t = struct
+  type t = S.t
+
+  let show v =
+    let width = 60 in
+    let buf = Buffer.create 100 in
+    PPrint.ToBuffer.pretty 1. width buf (S.layout v);
+    Buffer.contents buf
+
+  let print ?label v =
+    match label with
+    | Some label -> Caml.print_endline (label ^ ": " ^ show v)
+    | None -> Caml.print_endline (show v)
+end
+
+module type DUMPABLE = sig
+  type t
+
+  val dump : ?label:string -> t -> unit
+
+  val sdump : ?label:string -> t -> string
+end
+
+module Dumpable (S : sig
+  type t
+
+  val sexp_of_t : t -> Sexp.t
+end) : DUMPABLE with type t = S.t = struct
+  type t = S.t
+
+  let dump ?label v =
+    let s = S.sexp_of_t v in
+    match label with
+    | None -> Caml.Format.printf "%a@." Sexp.pp_hum s
+    | Some label -> Caml.Format.printf "%s %a@." label Sexp.pp_hum s
+
+  let sdump ?label v =
+    let s = S.sexp_of_t v in
+    match label with
+    | None -> Caml.Format.asprintf "%a@." Sexp.pp_hum s
+    | Some label -> Caml.Format.asprintf "%s %a@." label Sexp.pp_hum s
+end