8

In researching type inference differences between F# and OCaml I found they tended to focus on nominative vs. structural type system. Then I found Distinctive traits of functional programming languages which list typing and type inference as different traits.

Since the trait article says OCaml and F# both use Damas-Milner type inference which I thought was a standard algorithm, i.e. an algorithm that does not allow for variations, how do the two traits relate? Is it that Damas-Milner is the basis upon which both type inference systems are built but that they each modify Damas-Milner based on the typing?

Also I checked the F# source code for the words Damas, Milner and Hindley and found none. A search for the word inference turned up the code for type inference.

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

EDIT

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

Guy Coder
  • 24,501
  • 8
  • 71
  • 136
  • I wouldn't primarily look at the source code of compilers for something like this, instead I would first look at the specification of the languages. – svick Sep 09 '12 at 18:52
  • @GuyCoder Just curious -- which proof assistant are you porting? If it's open source, I'd be happy to help where I can -- just send me an email (see my profile page) to get in touch. – Jack P. Sep 09 '12 at 20:18
  • Of interest - see slide `Structural vs. Physical Equality` [An Introduction to Objective Caml](http://www.cs.columbia.edu/~sedwards/classes/2011/w4115-fall/ocaml.pdf) – Guy Coder Apr 13 '16 at 13:35

3 Answers3

6

Concerning your DM question, you are right. For both F# and OCaml, DM algorithm is just a pattern. Type checkers are extended to support custom features. In OCaml these features include objects with row types, poly variants, first-class modules. In F# - .NET type system interop (classes, interfaces, structs, subtyping, method overloads), units of measure. I think F# type inference is also skewed in a left-to-right fashion to allow more efficient interactive checking, therefore some code surprisingly needs annotations.

As far as type checking and inference goes, OCaml is more expressive and intuitive than F#. SML would be closer than either of them to a vanilla HM, but SML also has a few extensions for some operator polymorphism and record support.

t0yv0
  • 4,714
  • 19
  • 36
  • 2
    +1 but I don't think the difference is left-to-right but, rather, nominal vs structural. – J D Sep 14 '12 at 21:55
4

I believe that when they talk about structural typing in OCaml, they are probably referring to the object system (the "O" part of "OCaml"). The non-object parts of OCaml are pretty standard ML type system; it's the object system that is unusual.

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

Look at what happens when you write a function that takes an object and calls a particular method on it:

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

The argument type is inferred to be an abstract type that includes a method named bar. So it can take any object with such a method and type.

That's what it means when they say that the object system is structurally-typed. The only things that matter about an object is its set of methods, which determines where it can be used. So compatibility is just based on the "structure" of methods. And not on any idea of "class".

newacct
  • 119,665
  • 29
  • 163
  • 224
  • 1
    It might be worth pointing out that ML module system (and the flavor used in OCaml) uses structural typing as well (in signature matching), and F# does not even have one. – t0yv0 Sep 11 '12 at 12:07
  • "The non-object parts of OCaml are pretty standard ML type system; it's the object system that is unusual". Polymorphic variants are one obvious counter example and there are many others. – J D Sep 14 '12 at 07:15
  • "In OCaml, you can create objects directly without using a class". You can in F# too. – J D Sep 14 '12 at 07:16
2

Since the trait article says OCaml and F# both use Damas-Milner type inference which I thought was a standard algorithm, i.e. an algorithm that does not allow for variations, how do the two traits relate?

The Damas-Milner algorithm (also known as Algorithm W) can be extended and, indeed, all practically-relevant implementations of it have added many extensions including both OCaml and F#.

Is it that Damas-Milner is the basis upon which both type inference systems are built but that they each modify Damas-Milner based on the typing?

Exactly, yes. In particular, OCaml has a great many different experimental extensions to a Damas-Milner core including polymorphic variants, objects, first-class modules. F# is simpler but also has some extensions that OCaml does not have, most notably overloading (primarily operators).

I don't believe there are summary papers describing the whole type systems of either OCaml or F#. Indeed, I do not know of a paper that describes today's F# type system. For OCaml, you have many different papers each covering different aspects. I would start with Jacques Garrigue's own publications and then follow the references therein.

J D
  • 48,105
  • 13
  • 171
  • 274