Converting OCaml to F #: Differences between Typing and Output Type

Question

When researching the type of inference of the difference between F # and OCaml, I found that they tend to focus on a nominative versus a structural type system . Then I found the Distinctive features of functional programming languages that enumerate typing and introduce type as different features.

Since the featured article says that OCaml and F # use the Damas-Milner method, which I thought was a standard algorithm, that is, an algorithm that does not allow variations, how are the two features related? Is it that Damas-Milner is the foundation on which type inference systems are built, but each of them modifies Damas-Milner based on input?

I also checked the F # source code for the words Damas, Milner and Hindley and did not find any. A search for the output of the word called the type inference code.

If so, are there any documents that discuss the details of each type inference algorithm for a particular language, or should I look at the source code for OCaml and F # .

EDIT

Here is a page that highlights some of the differences related to type inference between OCaml and F #.

Answer 1

Since the featured article says that OCaml and F # use output like Damas-Milner, which, as I thought, is a standard algorithm, that is, an algorithm that does not allow variations, how are the two features related?

The Damascus-Milner Algorithm (also known as the W Algorithm) can be extended, and, indeed, all its practically relevant implementations have added many extensions, including OCaml and F #.

Is it that Damas-Milner is the foundation on which type inference systems are built, but each of them modifies Damas-Milner based on input?

Right, yes. In particular, OCaml has many different experimental extensions to the Damas-Milner core, including polymorphic options, objects, first-class modules. F # is simpler, but also has some extensions that OCaml does not have, primarily overloading (mostly operators).

I do not believe that there are summary articles describing systems of all type OCaml or F #. Indeed, I do not know a document that describes the F # type system today. For OCaml, you have many different documents, each of which covers various aspects. I would start my own publications with Jacques Garrigue , and then follow the links in it.

Answer 2

Regarding your question about DM, you're right. For both F # and OCaml, the DM algorithm is just a template. Type templates are expanded to support custom functions. In OCaml, these functions include objects with string types, poly variants, first-class modules. In F # -.NET, the type of system interaction (classes, interfaces, structures, subtyping, method overloads), units. I think that type F # output is also skewed left-right to provide a more efficient interactive check, so some code suddenly needs annotations.

Regarding type checking and output, OCaml is more expressive and intuitive than F #. SML will be closer than any of them to vanilla HM, but SML also has several extensions for some operator polymorphism and write support.

Answer 3

I believe that when they talk about structural typing in OCaml, they probably refer to the object system (part "O" "OCaml"). Parts that are not OCaml objects are a fairly standard ML type system; This is an unusual object system.

The object system in OCaml is very different from the object system of the .NET class in F #. In OCaml, you can create objects directly without using a class. And classes are basically a convenient feature for creating objects. An object after creation (created directly using a literal or using a class) has no idea about its class.

See what happens when you write a function that takes an object and calls a specific method on it:

# let foo x = x#bar;; val foo : < bar : 'a; .. > -> 'a = <fun> 

The type of the argument is defined as an abstract type that includes a method called bar . Therefore, he can take any object with this method and type.

What this means when they say that the object system is structured. The only thing that matters to an object is its set of methods, which determines where it can be used. Therefore, compatibility is based only on the "structure" of methods. And not on the idea of ​​"class".