Module signature with GADT

Is there a way to create module signature that has a polymorphic type variable like below? i.e. let meta : meta<'a>.

type expression = {expr: string}
type structure = {structure: string}

type rec modifier<'a> =
  | MExpression : modifier<expression>
  | MStructure : modifier<structure>

type meta<'a> = {
  proxy: modifier<'a>,
  callback: 'a => unit
}

module type HasRule = {
  let meta : meta<'a>
}

module Implementation: HasRule = {
  let callback = (expr) => {
    let _ = expr.expr
    ()
  }
  let meta = {
    proxy: MExpression,
    callback: callback
  }
}

The above code returns an error

  Values do not match:
    let meta: meta<expression>
  is not included in
    let meta: meta<'a>

I can introduce a type variable t to fix this but I’d like not to do that because I’d like to limit what t can be based on the modifier GADT. The idea is to use the type variable from GADT as type witness for the callback.

type expression = {expr: string}
type structure = {structure: string}

type rec modifier<'a> =
  | MExpression : modifier<expression>
  | MStructure : modifier<structure>

type meta<'a> = {
  proxy: modifier<'a>,
  callback: 'a => unit
}

module type HasRule = {
  type t
  let meta : meta<t>
}

module Implementation: HasRule = {
  type t = expression
  let callback = (expr) => {
    let _ = expr.expr
    ()
  }
  let meta = {
    proxy: MExpression,
    callback: callback
  }
}

Maybe I’m approaching this wrong. Can someone shed some light?

Thank you.

Edit: I am writing this in OCaml actually and if there’s a way OCaml can do this too it’d be great.

Can you explain what is the core problem you are trying to solve? We can only see some pieces of the implementation here, it’s hard to tell if the approach is good or needs adjustment.

I think my example can be reduced to

type expression = {expr: string}
type structure = {structure: string}

type rec modifier<'a> =
  | MExpression: modifier<expression>
  | MStructure: modifier<structure>

module type HasRule = {
  let someField: modifier<'a>
}

module Implementation1: HasRule = {
  let someField = MExpression
}

module Implementation2: HasRule = {
  let someField = MStructure
}

How do I type the module signature to be polymorphic? i.e. let someField : modifier<'a> without introducing type t in the module signature.

I want to say that the module needs to have a field someField which of type modifier but it can only be either modifier<expression> or modifier<structure>.

Is this possible?

If I understood correctly you want the type to be both polymorphic and constrained at the same time, hence not polymorphic, so I don’t think that’s possible. What’s wrong with introducing a type in the module signature? I’m still not sure of how you plan to use this though.

I want to introduce a type witness to my type so that the type 'a in the callback is inferred by the proxy.

type meta<'a> = {
  proxy: modifier<'a>,
  callback: 'a => unit
}

module type HasRule = {
  let meta : meta<'a>
}

module Implementation: HasRule = {
  // x here has type expression because proxy is of type modifier<expression>
  let callback = (x) => {
    let _ = x.expr
    ()
  }
  let meta = {
    proxy: MExpression,
    callback: callback
  }
}

module Implementation2: HasRule = {
  // x here has type structure because proxy is of type modifier<structure>
  let callback = (x) => {
    let _ = x.structure
    ()
  }
  let meta = {
    proxy: MStructure,
    callback: callback
  }
}

I need GADT because I have some part outside of this that requires me to pattern match on the constructors.

Why not having type t? It’d be nice not to have to write the type twice if the type can be inferred correctly. My current solution is to introduce type t. I’m curious to know if there’s a way to do this.

Well you your value meta is not polymorphic by definition, so you have to give it a non-polymorphic type, because on the contrary the type is correctly inferred as non-polymorphic by the type system.

You’re saying you don’t want to write the type twice, but you’d define it actually once in a working example:

type expression = {expr: string}
type structure = {structure: string}

type rec modifier<'a> =
  | MExpression: modifier<expression>
  | MStructure: modifier<structure>

type meta<'a> = {
  proxy: modifier<'a>,
  callback: 'a => unit,
}

module type HasRule = {
  type modifier
  let meta: meta<modifier>
}

module Implementation: HasRule = {
  type modifier = expression
  // x here has type expression because proxy is of type modifier<expression>
  let callback = x => {
    let _ = x.expr
  }
  let meta = {
    proxy: MExpression,
    callback: callback,
  }
}

module Implementation2: HasRule = {
  type modifier = structure
  // x here has type structure because proxy is of type modifier<structure>
  let callback = x => {
    let _ = x.structure
  }
  let meta = {
    proxy: MStructure,
    callback: callback,
  }
}
1 Like

Yes, that’s correct. That was my solution for now too. Please see my comment below for type modifier = expression.

module Implementation: HasRule = {
  // I want to avoid this line because `proxy` field already carries the proper type. 
  // Having to define the type here seems redundant
  type modifier = expression
  // x here has type expression because proxy is of type modifier<expression>
  let callback = x => {
    let _ = x.expr
  }
  let meta = {
    proxy: MExpression,
    callback: callback,
  }
}

I’m guessing that it is not possible - I’d need to define it in order to make it work.

1 Like

Actually, the compiler does correctly infer the type thanks to the proxy field, if you just remove the module type it will compile and will be inferred as what it is:

module Implementation = {
  // x here correctly inferred as type expression because proxy is of type modifier<expression>
  let callback = x => {
    let _ = x.expr
  }
  let meta = {
    proxy: MExpression,
    callback: callback,
  }
}

The error you have comes from the fact you want to give this module a signature, and inside this signature, meta can’t be polymorphic because it’s not polymorphic! So how else would you define meta type without giving it a concrete type?

4 Likes