CODEWITHSUNDEEP
f#type-inferencetyping
Guy Coder
Guy Coder

Reputation: 24976

F# typing rules as inference rules

Since F# uses type inferencing and type inferencing uses type rules, where are the F# type rules expressed as inference rules found. I suspect they are not published, easily located, or even available as inference rules, which why I am asking.

Googling F# type rules returns nothing relevant.

Searching the F# spec gives an interpretation in section 14 - Inference Procedures but does not give the actual rules.

I know I could extract them by reading the F# source code, (Microsoft.FSharp.Compiler.ConstraintSolver) but that could take time to extract and verify. Also while I am versed with Prolog which gives me some help in understanding the constraint solver, there is still a learning curve for me to read it.

Upvotes: 2

Views: 131

Answers (1)

Tomas Petricek
Tomas Petricek

Reputation: 243041

You are correct in that a formal specification of the F# type inference and type checking would be written using the format of inference rules.

The problem is that any realistic programming language is just too complicated for this kind of formal specification. If you wanted to capture the full complexity of the F# type inference, then you'd be just using mathematical notation to write essentially the same thing as what is in the F# compiler source code.

So, programming language theoreticians usually write typing and inference rules for some interesting subsets of the whole system - to illustrate issues related to some new aspect.

  • The core part of the F# type system is based on the Standard ML language. You can find a reasonable subset of ML formally specified in The Definition of Standard ML (PDF). This explains some interesting things like the "value restriction" rule.

  • I did some work on formalizing how the F# Data library works and this includes a simple model of bits of type checking for provided types, which you can find in F# Data paper.

  • The F# Computation Zoo paper (PDF) defines typing rules for how F# computation expression works. This actually captures typical use cases rather than what the compiler does.

In summary, I don't think it's feasible to expect formal specification of F# type inference in terms of typing rules, but I don't think any other language really has that. Formal models of languages are used more for exploring subtleties of little subsets, rather than for talking about the whole language.

Upvotes: 3

Related Questions