Type inference

.gitignore

@@ -133,6 +133,7 @@ pythontex-files-*/
 # Texpad
 .texpadtmp
 
+
 # TikZ & PGF
 *.dpth
 *.md5
@@ -158,4 +159,6 @@ pythontex-files-*/
 # Latexian
 TSWLatexianTemp*
 
-patterns-paper.pdf
+type-inference-paper.pdf
+
+*/_build

.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+    "cmake.configureOnOpen": false
+}

Makefile

@@ -1,4 +1,4 @@
-MAIN=patterns-paper
+MAIN=type-inference-paper
 
 all:
 	pdflatex $(MAIN)

_build/default/.dune/configurator

@@ -0,0 +1,2 @@
+(ocamlc /home/maroofr/.opam/ocaml-base-compiler.4.08.1/bin/ocamlc.opt)
+(ocaml_config_vars (afl_instrument false) (architecture amd64) (asm as) (asm_cfi_supported true) (ast_impl_magic_number Caml1999M025) (ast_intf_magic_number Caml1999N025) (bytecomp_c_compiler "gcc -O2 -fno-strict-aliasing -fwrapv -fcommon -fPIC -D_FILE_OFFSET_BITS=64 -D_REENTRANT") (bytecomp_c_libraries "-lm -ldl  -lpthread ") (c_compiler gcc) (cc_profile -pg) (ccomp_type cc) (cma_magic_number Caml1999A025) (cmi_magic_number Caml1999I025) (cmo_magic_number Caml1999O025) (cmt_magic_number Caml1999T025) (cmx_magic_number Caml1999Y025) (cmxa_magic_number Caml1999Z025) (cmxs_magic_number Caml1999D025) (default_executable_name a.out) (default_safe_string true) (exec_magic_number Caml1999X025) (ext_asm .s) (ext_dll .so) (ext_exe "") (ext_lib .a) (ext_obj .o) (flambda false) (flat_float_array true) (host x86_64-pc-linux-gnu) (int_size 63) (model default) (native_c_compiler "gcc -O2 -fno-strict-aliasing -fwrapv -fcommon -D_FILE_OFFSET_BITS=64 -D_REENTRANT") (native_c_libraries "-lm -ldl ") (native_pack_linker "ld -r -o ") (ocamlc_cflags "-O2 -fno-strict-aliasing -fwrapv -fcommon -fPIC") (ocamlc_cppflags "-D_FILE_OFFSET_BITS=64 -D_REENTRANT") (ocamlopt_cflags "-O2 -fno-strict-aliasing -fwrapv -fcommon") (ocamlopt_cppflags "-D_FILE_OFFSET_BITS=64 -D_REENTRANT") (os_type Unix) (profiling true) (ranlib ranlib) (safe_string false) (spacetime false) (standard_library /home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib/ocaml) (standard_library_default /home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib/ocaml) (supports_shared_libraries true) (system linux) (systhread_supported true) (target x86_64-pc-linux-gnu) (version 4.08.1) (windows_unicode false) (with_frame_pointers false) (word_size 64))

_build/default/.dune/configurator.v2

@@ -0,0 +1 @@
+((6:ocamlc61:/home/maroofr/.opam/ocaml-base-compiler.4.08.1/bin/ocamlc.opt)(17:ocaml_config_vars((14:afl_instrument5:false)(12:architecture5:amd64)(3:asm2:as)(17:asm_cfi_supported4:true)(21:ast_impl_magic_number12:Caml1999M025)(21:ast_intf_magic_number12:Caml1999N025)(19:bytecomp_c_compiler87:gcc -O2 -fno-strict-aliasing -fwrapv -fcommon -fPIC -D_FILE_OFFSET_BITS=64 -D_REENTRANT)(20:bytecomp_c_libraries20:-lm -ldl  -lpthread )(10:c_compiler3:gcc)(10:cc_profile3:-pg)(10:ccomp_type2:cc)(16:cma_magic_number12:Caml1999A025)(16:cmi_magic_number12:Caml1999I025)(16:cmo_magic_number12:Caml1999O025)(16:cmt_magic_number12:Caml1999T025)(16:cmx_magic_number12:Caml1999Y025)(17:cmxa_magic_number12:Caml1999Z025)(17:cmxs_magic_number12:Caml1999D025)(23:default_executable_name5:a.out)(19:default_safe_string4:true)(17:exec_magic_number12:Caml1999X025)(7:ext_asm2:.s)(7:ext_dll3:.so)(7:ext_exe0:)(7:ext_lib2:.a)(7:ext_obj2:.o)(7:flambda5:false)(16:flat_float_array4:true)(4:host19:x86_64-pc-linux-gnu)(8:int_size2:63)(5:model7:default)(17:native_c_compiler81:gcc -O2 -fno-strict-aliasing -fwrapv -fcommon -D_FILE_OFFSET_BITS=64 -D_REENTRANT)(18:native_c_libraries9:-lm -ldl )(18:native_pack_linker9:ld -r -o )(13:ocamlc_cflags47:-O2 -fno-strict-aliasing -fwrapv -fcommon -fPIC)(15:ocamlc_cppflags35:-D_FILE_OFFSET_BITS=64 -D_REENTRANT)(15:ocamlopt_cflags41:-O2 -fno-strict-aliasing -fwrapv -fcommon)(17:ocamlopt_cppflags35:-D_FILE_OFFSET_BITS=64 -D_REENTRANT)(7:os_type4:Unix)(9:profiling4:true)(6:ranlib6:ranlib)(11:safe_string5:false)(9:spacetime5:false)(16:standard_library56:/home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib/ocaml)(24:standard_library_default56:/home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib/ocaml)(25:supports_shared_libraries4:true)(6:system5:linux)(19:systhread_supported4:true)(6:target19:x86_64-pc-linux-gnu)(7:version6:4.08.1)(15:windows_unicode5:false)(19:with_frame_pointers5:false)(9:word_size2:64))))

_build/log

@@ -0,0 +1,131 @@
+# dune build test.exe
+# OCAMLPARAM: unset
+# Workspace root: /home/maroofr/type-inference-paper
+$ /usr/bin/nproc > /tmp/dunef44937.output 2> /dev/null
+# Auto-detected concurrency: 4
+# disable binary cache
+$ /home/maroofr/.opam/ocaml-base-compiler.4.08.1/bin/ocamlc.opt -config > /tmp/dune338217.output
+# Dune context:
+#  { name = "default"
+#  ; kind = "default"
+#  ; profile = Dyn
+#  ; merlin = true
+#  ; for_host = None
+#  ; fdo_target_exe = None
+#  ; build_dir = "default"
+#  ; toplevel_path =
+#      Some
+#        External "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib/toplevel"
+#  ; ocaml_bin = External "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/bin"
+#  ; ocaml =
+#      Ok External "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/bin/ocaml"
+#  ; ocamlc =
+#      External "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/bin/ocamlc.opt"
+#  ; ocamlopt =
+#      Ok
+#        External
+#          "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/bin/ocamlopt.opt"
+#  ; ocamldep =
+#      Ok
+#        External
+#          "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/bin/ocamldep.opt"
+#  ; ocamlmklib =
+#      Ok
+#        External
+#          "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/bin/ocamlmklib.opt"
+#  ; env =
+#      map
+#        { "DUNE_OCAML_HARDCODED" :
+#            "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib"
+#        ; "DUNE_OCAML_STDLIB" :
+#            "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib/ocaml"
+#        ; "DUNE_SOURCEROOT" : "/home/maroofr/type-inference-paper"
+#        ; "INSIDE_DUNE" : "/home/maroofr/type-inference-paper/_build/default"
+#        ; "OCAMLFIND_IGNORE_DUPS_IN" :
+#            "/home/maroofr/type-inference-paper/_build/install/default/lib"
+#        ; "OCAMLPATH" :
+#            "/home/maroofr/type-inference-paper/_build/install/default/lib"
+#        ; "OCAMLTOP_INCLUDE_PATH" :
+#            "/home/maroofr/type-inference-paper/_build/install/default/lib/toplevel"
+#        ; "OCAML_COLOR" : "always"
+#        ; "OPAMCOLOR" : "always"
+#        }
+#  ; findlib_path =
+#      [ External "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib" ]
+#  ; arch_sixtyfour = true
+#  ; natdynlink_supported = true
+#  ; supports_shared_libraries = true
+#  ; ocaml_config =
+#      { version = "4.08.1"
+#      ; standard_library_default =
+#          "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib/ocaml"
+#      ; standard_library =
+#          "/home/maroofr/.opam/ocaml-base-compiler.4.08.1/lib/ocaml"
+#      ; standard_runtime = "the_standard_runtime_variable_was_deleted"
+#      ; ccomp_type = "cc"
+#      ; c_compiler = "gcc"
+#      ; ocamlc_cflags =
+#          [ "-O2"; "-fno-strict-aliasing"; "-fwrapv"; "-fcommon"; "-fPIC" ]
+#      ; ocamlc_cppflags = [ "-D_FILE_OFFSET_BITS=64"; "-D_REENTRANT" ]
+#      ; ocamlopt_cflags =
+#          [ "-O2"; "-fno-strict-aliasing"; "-fwrapv"; "-fcommon" ]
+#      ; ocamlopt_cppflags = [ "-D_FILE_OFFSET_BITS=64"; "-D_REENTRANT" ]
+#      ; bytecomp_c_compiler =
+#          [ "gcc"
+#          ; "-O2"
+#          ; "-fno-strict-aliasing"
+#          ; "-fwrapv"
+#          ; "-fcommon"
+#          ; "-fPIC"
+#          ; "-D_FILE_OFFSET_BITS=64"
+#          ; "-D_REENTRANT"
+#          ]
+#      ; bytecomp_c_libraries = [ "-lm"; "-ldl"; "-lpthread" ]
+#      ; native_c_compiler =
+#          [ "gcc"
+#          ; "-O2"
+#          ; "-fno-strict-aliasing"
+#          ; "-fwrapv"
+#          ; "-fcommon"
+#          ; "-D_FILE_OFFSET_BITS=64"
+#          ; "-D_REENTRANT"
+#          ]
+#      ; native_c_libraries = [ "-lm"; "-ldl" ]
+#      ; cc_profile = [ "-pg" ]
+#      ; architecture = "amd64"
+#      ; model = "default"
+#      ; int_size = 63
+#      ; word_size = 64
+#      ; system = "linux"
+#      ; asm = [ "as" ]
+#      ; asm_cfi_supported = true
+#      ; with_frame_pointers = false
+#      ; ext_exe = ""
+#      ; ext_obj = ".o"
+#      ; ext_asm = ".s"
+#      ; ext_lib = ".a"
+#      ; ext_dll = ".so"
+#      ; os_type = "Unix"
+#      ; default_executable_name = "a.out"
+#      ; systhread_supported = true
+#      ; host = "x86_64-pc-linux-gnu"
+#      ; target = "x86_64-pc-linux-gnu"
+#      ; profiling = true
+#      ; flambda = false
+#      ; spacetime = false
+#      ; safe_string = false
+#      ; exec_magic_number = "Caml1999X025"
+#      ; cmi_magic_number = "Caml1999I025"
+#      ; cmo_magic_number = "Caml1999O025"
+#      ; cma_magic_number = "Caml1999A025"
+#      ; cmx_magic_number = "Caml1999Y025"
+#      ; cmxa_magic_number = "Caml1999Z025"
+#      ; ast_impl_magic_number = "Caml1999M025"
+#      ; ast_intf_magic_number = "Caml1999N025"
+#      ; cmxs_magic_number = "Caml1999D025"
+#      ; cmt_magic_number = "Caml1999T025"
+#      ; natdynlink_supported = true
+#      ; supports_shared_libraries = true
+#      ; windows_unicode = false
+#      }
+#  }

abstract.tex

@@ -0,0 +1,7 @@
+% !TEX root = hazel-LIVE2018.tex
+
+\begin{abstract}
+\emph{Type inference} allows programmers to omit type annotations while still permitting type checking. The problem is that \emph{type inference} only works on complete programs, e.g. syntactically well-formed expressions. This paper introduces a \emph{type hole inference} system that applies type inference on incomplete programs. We start from modeling incomplete programs by lambda calculus with \emph{holes} developed in \Hazelnut, where holes stand for missing types and expressions. We extended static semantics with \emph{type constraints}, and borrow machinery from unification-based type inference to infer types for type holes by identifying the type hole with the type variable. In particular, our system will not report a static error when unification fails but postpone type-checking for type holes to runtime. This provides an approach to combine \emph{gradual typing} and \emph{type inference}. 
+
+\end{abstract}
+