tomprimozic / type-systems Goto Github PK

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.

A question, possibly stemming from a misunderstanding on my part

In this function a hash table is created.

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.

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?

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.

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, 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.

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?

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?

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