tomprimozic / type-systems Goto Github PK
View Code? Open in Web Editor NEWImplementations of various type systems in OCaml.
License: The Unlicense
Implementations of various type systems in OCaml.
License: The Unlicense
First of all, I would like to say thank you for your great project on type systems. I've been interested in the concept for a while without never really touching or implementing them and your project really helps me to better understand them.
I've always thought that a perfect type system would be something along two of your sub-projects, first class polymorphism + refined types. I've been playing around with those two a little bit with the hope of merging them but I wanted to ask you first if it made sense since you seem to be well versed on the subject. Is there anything that would prevent them both from co-existing within the same type system?
I believe as when using types as documentations, top level annotations could be much more readable.
HMF implemented in this repo allows following notations:
let f = fun (f: some a. forall b. b -> a -> a) b a -> f b a
However, I wonder if this is valid is HMF:
let f: forall a. (forall b. b -> a -> a) ->
forall b. b -> a -> a =
fun g -> fun a -> fun b -> g b a
I believe annotating as the second way is more nice to have, but my re-implementation of FSP given in this repo shows that some complex top level annotations cannot pass type inference and checking.
Any workaround, or just some ideas?
Hi, thank you for interesting implementations.
These type systems are implemented for tiny language. It contains Var
, Call
, Fun
and Let
expressions. While reading your algorithm_w
implementation, I noticed that they lack important functional programming feature: recursive functions.
For recursive functions, type inference sometimes needs to care about them. Before applying type inference, type variable for the function should be added to type environment because function body may contain applying itself (recursive call).
For example, assume let rec
exists and let's say to write let rec f x = f 10; 42 in f true
. When visiting the LetRec
node, inferrer makes type variable for f
to type environment before apply type analysis to function body f 10; 42
for recursive function call. And then applies type inference to f 10
. In function body, the type of f
is determined to int -> int
. This works for monomorphic function. But in this case, f
is a polymorphic function 'a -> int
. But function type is determined before generalized. Hence f true
will fail after because of int -> int
type. I feel some trick is necessary to support recursive function. What do you think about this?
A question, possibly stemming from a misunderstanding on my part
In this function a hash table is created.
type-systems/algorithm_w/infer.ml
Line 87 in 7c4f5d3
It is used in the TVar {contents = Generic id}
branch, where the table is updated with a var if it does not already contain it.
type-systems/algorithm_w/infer.ml
Lines 92 to 97 in 7c4f5d3
If I'm not misreading, the recursive function terminates immediately after the new var is added to the hashtable, causing the table to go out of scope and be deallocated.
With this in mind it seems like the hashtable is never used and could be removed. Is this correct?
There is Complexity Zoo. Do you have any plans to create (start) the same type of resource for different type systems?
Each section could contain: name, features, links to theoretical papers (if any), example of programming language.
P.S. thank you for this repo.
Hello, I am pretty new to the Ocaml type system but I'll like to use the refined type. So please, can you give me a small walkthrough on how I can go about to use this system or the code in your repository? The latest version of Ocaml is installed in my machine already.
Thanks.
Hi, Im just querying if this section is correct:
https://github.com/tomprimozic/type-systems/blob/master/extensible_rows/infer.ml#L78-L83
| TRowExtend(label1, field_ty1, rest_row1), (TRowExtend _ as row2) -> begin
let rest_row1_tvar_ref_option = match rest_row1 with
| TVar ({contents = Unbound _} as tvar_ref) -> Some tvar_ref
| _ -> None
in
let rest_row2 = rewrite_row row2 label1 field_ty1 in
begin match rest_row1_tvar_ref_option with
| Some {contents = Link _} -> error "recursive row types"
| _ -> ()
end ;
unify rest_row1 rest_row2
end
rest_row1_tvar_ref_option
is Some
when contents = Unbound
yet the check to throw on recursion tests for a Link
which will never be matched.
I've recently been looking around at System FC, which is what is used in haskell. I don't know if you've heard of it but it's interesting.
https://www.youtube.com/watch?v=2IZQx7WNOMs
https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/FC_in_GHC_July13.pdf
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.