I can live within those constraints

I’ve just spent a little time reading the F# specification.

I must confess that I hadn’t come across the upcast and downcast functions before, which can be used to change the type associated with a value.

> let x : obj = upcast “hello”;;
val x : obj = “hello”
> let y : string = downcast x;;
val y : string = “hello”

My main reason for reading the specification was to get a better mental model of the type system that the language uses. In the past I was part of a team that implemented an ML compiler. This used a variant of the Hindley-Milner type checking algorithm. In contrast, the F# system type checks types using constraint solving, and there are a lot more types of constraint that need to be checked.

> type First() = class end;;
> type Second() = class inherit First() end;;

> let f x : ‘T when ‘T :> First = x;;
val f : ‘T -> ‘T when ‘T :> First

The :> constraint demands a subtype relationship between the argument and the target type.

> f(First());;
val it : First = FSI_0005+First
> f(Second());;
val it : Second = FSI_0006+Second

and has a short form using the hash symbol.

> let f x : #First = x;;
val f : ‘a -> ‘a when ‘a :> First

The member constraint can be used to ensure that a type supports a certain operation. It is used in conjunction with type variables that cannot be generalised and which are written in the form ^T.

> let f x : ^a = x;;
  let f x : ^a = x;;
stdin(14,12): warning FS0064: This construct causes code to be less generic than
indicated by the type annotations. The type variable ‘a has been constrained to
be type ‘obj’.
val f : obj –> obj

Because of this lack of generalisation, the ^ types are most often used in the context of inline functions.

> let inline doit (x: ^a) = (^a : (static member speak: int -> string) (20));;
val inline doit :
   ^a -> string when  ^a : (static member speak : int -> string)

The previous function ensures that the argument is of a type that has a static member called speak.

> type Boo() = static member speak x = “Called on ” + x.ToString();;
> doit(Boo());;
val it : string = “Called on 20”

It took me quite a while to figure out how to call a non-static member, mainly because I failed to notice that a tuple was required to apply the member.

> let inline doit (x: ^a) = (^a : (member speak: int -> string) (x,20));;
val inline doit :
   ^a -> string when  ^a : (member speak :  ^a * int -> string)

> type Test3() = class member x.speak(y) = “Hello” end;;
> doit(Test3());;
val it : string = “Hello”

F# is great in that it discourages the use of null as a member of lots of datatypes. We can constrain a function to take an argument that is of a type that has null as a member:

> let f x : ‘a when ‘a : null = x;;

This function works on standard .NET classes like string, which have null as a member.

> f “hello”;;
val it : string = “hello”

But not on the typical F# datatypes which do not have a null member.

> type Foo = A | B;;
> f A;;
  f A;;
stdin(20,3): error FS0001: The type ‘Foo’ does not have ‘null’ as a proper value

We can constrain on types that have a particular constructor:

> let f x : ‘a when ‘a : (new : unit -> ‘a) = x;;

And much like C# generics we can demand a valuetype

> let f x : ‘a when ‘a : struct = x;;
> f “hello”;;
  f “hello”;;
stdin(28,3): error FS0001: A generic construct requires that the type ‘string’ is a CLI or F# struct type
> f System.DateTime.Now;;
val it : System.DateTime = 03/12/2010 18:55:33 {Date = 03/12/2010 00:00:00;

or a reference type.

> let f x : ‘a when ‘a : not struct = x;;
> f “hello”;;
val it : string = “hello”
> f System.DateTime.Now;;
  f System.DateTime.Now;;
stdin(33,3): error FS0001: A generic construct requires that the type ‘System.DateTime’ have reference semantics, but it does not, i.e. it is a struct

One can demand types that are unmanaged or delegate types.

> let f x : ‘a when ‘a : unmanaged = x;;
> f “hello”;;
  f “hello”;;
stdin(39,3): error FS0001: A generic construct requires that the type ‘string’ is an unmanaged type

> let handler = Microsoft.Win32.TimerElapsedEventHandler(fun o ev –> ());;
val handler : Microsoft.Win32.TimerElapsedEventHandler

> let f x : ‘a when ‘a : delegate<Microsoft.Win32.TimerElapsedEventArgs,unit> =x;;
val f :  ‘a -> ‘a when ‘a : delegate<Microsoft.Win32.TimerElapsedEventArgs,unit>

> f handler;;
val it : Microsoft.Win32.TimerElapsedEventHandler = …

For interoperability there’s a also a way to specify the underlying type for an enumeration.

> let f x : ‘T when ‘T : enum<int> = x;;
val f : ‘T -> ‘T when ‘T : enum<int>

> f(System.Diagnostics.TraceOptions.DateTime);;
val it : System.Diagnostics.TraceOptions = DateTime

Most importantly, you can demand types that support equality or comparison.

> [<NoEquality;NoComparison>]
– type Foo() =
–   class end;;
> let f x : ‘a when ‘a : equality = x;;
val f : ‘a -> ‘a when ‘a : equality

> f 2;;
val it : int = 2
> f (Foo());;
  f (Foo());;
stdin(91,4): error FS0001: The type ‘Foo’ does not support the ‘equality’ constraint because it has the ‘NoEquality’ attribute

> let f x : ‘a when ‘a : comparison = x;;
val f : ‘a -> ‘a when ‘a : comparison
> let t = new System.GenericUriParser(System.GenericUriParserOptions.NoQuery);;
> f t;;
  f t;;
stdin(69,3): error FS0001: The type ‘System.GenericUriParser’ does not support the ‘comparison’ constraint. For example, it does not support the ‘System.IComparable’ interface

It is also worth pointing out that you can have multiple constraints.

> let f x : ‘a when ‘a : not struct and ‘a : comparison = x;;
val f : ‘a -> ‘a when ‘a : not struct and ‘a : comparison

The system takes the various constraints on the type variable, and the constraints that are generated from the structure of the program and attempts to find a solution to them.

For example, suppose that we know f : string * int –> int and we need to check the following function definition.

  let g x y = f(x, f(x, 10))

We’d generate new type variables ty1, ty2 and ty3 and the constraints
    g : ty1 –> ty2 –> ty3
The inner application would involve a new variable ty4 and the constraints
  ty4 : int,  ty1 : string
And the outer application would give
  ty1 : string, ty4 : int, ty3:int

Solving the constraints would give the solution with ty1 = string, ty3 = int and ty2 as anything. We could therefore infer the type of g as
  val g : string -> ‘a -> int

This entry was posted in Computers and Internet. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s