GADT and polymorphic recursion

Learning
,
1

I’m writing some code about OCaml’s typedtree, my current result is too long and complex, and I want to make it better.

Right now I have solutions that use 1) locally abstract types, and 2) non-prenex polymorphism via record, or 2) open recursion. Is it possible to abandon records for non-prenex polymorphism?

This one has all three features:

  (* OCaml 3.12.1 *)
  open Typedtree
  type ttt = { self : 'a . 'a pattern_desc pattern_data -> bool}

  (* Kind of what I want but long *)
  let _hack =
    let helper (type a)
        (self : ttt)
        (p1: a Typedtree.pattern_desc pattern_data)  =
      match p1.pat_desc with
      | Tpat_any
      | Tpat_var _ -> true
      | Tpat_constant c1 -> true
      | Tpat_tuple t1 -> List.for_all self.self t1
      | Tpat_construct (_, cd1, a1) -> List.for_all self.self a1
      | Tpat_value v1 ->
          self.self
            (v1 :> Typedtree.pattern)
      | Tpat_exception _
      | _ -> false
    in
    let rec ans  = { self = (fun eta -> helper ans eta) } in
    ans

If I abondon only open recursion it compiles too:

  let _hack_no_open_recursion =
    let rec helper = { self = (fun (type a)  (p1: a Typedtree.pattern_desc pattern_data)  ->
      match p1.pat_desc with
      | Tpat_any
      | Tpat_var _ -> true
      | Tpat_constant c1 -> true
      | Tpat_tuple t1 -> List.for_all helper.self t1
      | Tpat_construct (_, cd1, a1) -> List.for_all helper.self a1
      | Tpat_value v1 ->
          helper.self
            (v1 :> Typedtree.pattern)
      | Tpat_exception _
      | _ -> false
    )}
    in
    helper

If I abandone non-prenex polymorphism and open recursion, I would get a wrong type

  (* `value general_pattern -> bool` Not what I want *)
  let rec _hack_bad2  (type a) (p1: a Typedtree.pattern_desc pattern_data) =
      match p1.pat_desc with
      | Tpat_any
      | Tpat_var _ -> true
      | Tpat_constant c1 -> true
      | Tpat_tuple t1 -> List.for_all _hack_bad2 t1
      | Tpat_construct (_, cd1, a1) -> List.for_all _hack_bad2 a1
      | Tpat_value v1 ->
          _hack_bad2
            (v1 :> value Typedtree.pattern_desc Typedtree.pattern_data) 
      | Tpat_exception _
      | _ -> false

And when I abondon only non-prenex polymorphism I get compilation error

  let _hack_bad =
    let helper (type a)
        (self : a pattern_desc pattern_data -> bool)
        (p1: a Typedtree.pattern_desc pattern_data)  =
      match p1.pat_desc with
      | Tpat_any
      | Tpat_var _ -> true
      | Tpat_constant c1 -> true
      | Tpat_tuple t1 -> List.for_all self t1
      | Tpat_construct (_, cd1, a1) -> List.for_all self a1
      | Tpat_value v1 ->
          self
            (v1 :> value Typedtree.pattern_desc Typedtree.pattern_data)
          (*
          Error: This expression has type value Typedtree.pattern_desc pattern_data
                but an expression was expected of type
                  a Typedtree.pattern_desc pattern_data
                Type value is not compatible with type a
          *)
      | Tpat_exception _
      | _ -> false
    in
    let rec ans eta = helper ans eta in
    ans
2

You may use the polymorphic syntax for locally abstract type, which allows you to use polymorphic recursion directly.

let rec check : type a . a pattern_desc pattern_data -> bool = fun p1 ->
  match p1.pat_desc with
  | Tpat_any
  | Tpat_var _ -> true
  | Tpat_constant _c1 -> true
  | Tpat_tuple t1 -> List.for_all check t1
  | Tpat_construct (_, _cd1, a1) -> List.for_all check a1
  | Tpat_value v1 ->
      check (v1 :> Typedtree.pattern)
  | Tpat_exception _
  | _ -> false
1 Like