Is it possible to use GADTs with default arguments?

Learning
5

In brief, you cannot have a default type with the standard option type.

When the label layer is removed, your function is equivalent to:

let unbox_default (type t) (c:t container option)  =
  let opt = match c with
    | Some c -> c
    | None -> Int i
  in
  match opt with
  | Int i -> i
  | String s -> s
  | Bool b -> b

which fails with

      but an expression was expected of type t container
      Type int is not compatible with type t

because the default case Int i can only work for int containers.

The problem is thus that the type that we want for unbox_default is not

t container option -> t

but something like

<default:int container; ty:t container> option' -> t

So let’s write such option' type :

type _ option' =
| Nothing : <default:'d; ty:'d> option'
| Just: 'ty -> <default:'d; ty:'ty> option'

With this, we can rewrite the long form of the unbox_default to:

let unbox_default (type t) 
  (c:<default:int container; ty:t container> option'): t  =
  let opt = match c with
    | Just c -> c
    | Nothing -> Int 0
  in
  match opt with
  | Int i -> i
  | String s -> s
  | Bool b -> b

which has the expected behavior. Unfortunately (or not), this GADT variant of the option type is not the one used by optional labels.

3 Likes