OCaml - GADT mapping

Question

I'm struggling with understanding some aspects of using GADTs in OCaml. Let me try and talk you through my example and my understanding ...

I'm trying to implement Simon Peyton-Jones' classic paper on Combinatorial Contracts (https://www.microsoft.com/en-us/research/wp-content/uploads/2000/09/pj-eber.pdf)

I want to be able to manipulate an Observable, defined as a function from a date to a value of some type (realistically a float or a bool). So, using GADTs I define a function type and an Observation type

type _ value = 
| Float : float -> float value
| Bool : bool -> bool value

type _ obs = Observation : (date -> 'v value) -> (date -> 'v) obs

What I think I am defining is that

a value is either a float or a bool (built using the Float or Bool constructors, and
an obs is a function from a date to one of the value types, so either a date -> float or a date -> bool

Now I define an expression, which enables me to combine Observables

type _ expr =
| Konst : 'v value -> 'v expr
| Obs : 'v obs -> 'v expr
| Lift : ('v1 -> 'v2) * 'v1 expr -> 'v2 expr

So far so good. An expression is either a constant, an observation (which is either a date->float or date->bool), or a function applied to an expression.

Now I want to be able to evaluate an Observable. In reality, an Observable is built on a random process, so I have a Distribution module (Note that in the original paper the idea is to separate out the concept of an Observable, from it's implementation - so we could implement through lattices, monte carlo, or whatever approach we want).

module type Distribution_intf =
  sig
    type element = Element of float * float
    type t = element list

    val lift : t -> f:(float -> float) -> t
    val expected : t -> float
  end

so, given a compose function let compose f g = fun x -> f (g x)

I should be able to think about the evaluation of an Observable. Here is a mapping function (I've taken out the Boolean case for clarity)

type rv = date -> Distribution.t

let rec observable_to_rv : type o. o Observable.expr -> rv = 
  let open Distribution in
  function
  | Konst (Float f) -> fun (_:date) -> [Element(1.0, f)]
  | Lift (f,obs) -> compose (lift ~f) (observable_to_rv o) (*ERROR HERE *)

Now things get problematic. When I try and compile, I get the following error message (on the Lift pattern match):

Error: This expression has type v1#0 -> o
   but an expression was expected of type float -> float
   Type v1#0 is not compatible with type float

I don't understand why: A Lift expression has type

Lift: ('v1 -> 'v2) * 'v1 expr -> 'v2 expr

So given a Lift(f,o), then shouldn't the compiler constrain that since observable_to_rv has type date -> float, then 'v2 must be a float, and since lift has type float -> float then 'v1 must be a float, so Lift should be defined on any tuple of type (float -> float, float expr).

What am I missing ?

Steve

octachron octachron · Accepted Answer · 2018-02-22T12:26:23

You are missing the fact that the type variable 'v1 in Lift is existentially quantified:

Lift: ('v1 -> 'v2) * 'v1 expr -> 'v2 expr

means

Lift: ∃'v1. ('v1 -> 'v2) * 'v1 expr -> 'v2 expr

In other words, given a value Lift(f,x): 'b expr the only information that the type checker has is that there is a type 'a such that f:'a -> 'b and x:'a expr, nothing more.

In particular going back to your error message (with a somewhat recent version of compiler(≥ 4.03)):

Type $Lift_'v1 is not compatible with type float

it is not possible to unify this existential type introduced by the Lift constructor to the float type, or any concrete type, because there no information left in the type system on the actual concrete type hidden behind 'v1 at this point.

EDIT: The essence of your problem is that you are trying to build a float random variable from a chain of expression 'a expr which can contain intermediary expressions of any type and just need to result with 'a expression. Since you can neither express the condition only float sub-expression in the type system nor construct non-float random variable with your current design, this spells trouble.

The solution is either to remove the ability to build non-float expression or to add the ability to handle non-float random variables .Taking the second option would look like

module Distribution:
  sig
    type 'a element = {probability:float; value: 'a}
    type 'a t = 'a element list

    val lift : 'a t -> f:('a -> 'b) -> 'b t
    val expected : float t -> float
  end = struct … end

Then your observable_to_rv random variable typed as 'a expr -> 'a rv will type-check.

OCaml - GADT mapping

1 Answers