Hot answers tagged

12

Have you seen Arthur Charguéraud's PhD thesis, Characteristic Formulae for Mechanized Program Verification? Rather than building the type system and small-step semantics as inductive relations, he gives a technique for converting Caml programs into characteristic formulas. This are basically a generalization of predicate transformer semantics to support a ...


8

You could be interested in Jacques Garrigue's A Certified Implementation of ML with Structural Polymorphism and Recursive Types, which establishes the soundness of static and dynamic semantics and properties of type inference for a ML language with (recursion and) structural polymorphism, thus formalizing one of the more advanced corners of OCaml (...


4

Your C# example doesn't trigger the value restriction at all. Here it is in OCaml: # let foo f init acc = let cur = ref init in (fun () -> cur := f !cur acc ; !cur) ;; val foo : ('a -> 'b -> 'a) -> 'a -> 'b -> unit -> 'a = <fun> # let my_bar_a = foo (+) 0 1 ;; val my_bar_a : unit -> int = <fun> # let my_bar_b = ...


2

However, I can easily make a C# function which captures a parameterized variable, and parametrically instantiate it over both int and string. The equivalent to code forbidden by value restriction would need a generic local variable of type which would be written something like Func<A, A> foo<A> = ..., which isn't legal in C# (though it isn't ...


Only top voted, non community-wiki answers of a minimum length are eligible