CODEWITHSUNDEEP
ocamltype-inference
Seneca
Seneca

Reputation: 2412

Ocaml incorrect type inference

I'm trying to make a typed version of React as an exercise in Ocaml. To make it more functional, I'm passing a record as argument to render.

type ('props,'state) reactInstance =
  {
  props: 'props;
  state: 'state;
  updater: 'a . ('props,'state) reactInstance -> 'a -> 'state -> unit;}
and ('props,'state) reactClass =
  {
  getInitialState: unit -> 'state;
  render: ('props,'state) reactInstance -> element;}

module type ComponentBluePrint  =
  sig
    type props
    type state
    val getInitialState : unit -> state
    val render : (props,state) reactInstance -> element
  end

module type ReactClass  =
  sig
    type props
    type state
    val mkUpdater :
  props ->
    ((props,state) reactInstance -> 'e -> state) ->
      (props,state) reactInstance -> 'e -> unit
    val reactClass : (props,state) reactClass
  end

module CreateComponent(M:ComponentBluePrint) =
  (struct
     include M
     let rec mkUpdater props f i e =
       let nextState = f i e in
       let newInstance =
         { props; state = nextState; updater = (mkUpdater props) } in
       ()

     let reactClass =
       { render = M.render; getInitialState = M.getInitialState }
   end : (ReactClass with type  props =  M.props and type  state =  M.state))

One thing I don't understand is why the compiler can't infer the type of updater = (mkUpdater props) in let newInstance = { props; state = nextState; updater = (mkUpdater props) }.

Error: Signature mismatch:
       Values do not match:
         let mkUpdater :
  props =>
  (reactInstance props state => '_a => '_b) =>
  reactInstance props state => '_a => unit
       is not included in
         let mkUpdater :
  props =>
  (reactInstance props state => 'e => state) =>
  reactInstance props state => 'e => unit

What's the difference between '_a and 'e ? It looks exactly to same to me. How do I make this type check?

Upvotes: 2

Views: 493

Answers (1)

ivg
ivg

Reputation: 35210

A type variable '_a (the actual letter doesn't matter, the crucial thing is the underscore) is a so called weak type variable. This is a variable that cannot be generalized, i.e., it can be substituted with only one concrete type. It is like a mutable value, but in the realm of types.

A type denoted with a weak type variable '_a is not included in a type that is denoted with a generic type variable. Moreover, it even can't escape the compilation unit, and should be either hidden or concretized.

Weak type variables are created when an expression is not a pure value (that is defined syntactically). Usually, it is either a function application, or an abstraction. It is usually possible, to get rid of weak type variables by doing a so called eta-expansion, when you substitute a partially applied function to a normal function application by enumerating all function arguments, i.e., updater = (fun props f i e -> mkUpdater props f i e).

Upvotes: 2

Related Questions