[Caml-list] GADT and optional arguments: Can they work?

[Goswin von Brederlow <goswin-v-b@web.de>]

Hi,

after having just written a ton of functions that just differ in the
argument type I started to think that this might be a good use acase for
GADT types.

So instead of seperate get_int, get_int32, get_int64, ... functions
there would only be one get function with an extra GADT argument to
specifiy the type to be used.


For example Unix.lseek and Unix.LargeFile.lseek could be written as:

(* GADT for LargeFile *)

type _ size = Int : int size | Int64 : int64 size

let lseek : type a . a size -> Unix.file_descr -> a -> Unix.seek_command -> a =
  fun size fd off cmd ->
    match size with
      | Int -> Unix.lseek fd off cmd
      | Int64 -> Unix.LargeFile.lseek fd off cmd

val lseek : 'a size -> Unix.file_descr -> 'a -> Unix.seek_command -> 'a = <fun>


So far so good. But now one has to specify the argument size on every
lseek call. To make it nicer I would like the size to be optional and
specify a default size for the most common use:

let lseek : type a . ?size:a size -> Unix.file_descr -> a -> Unix.seek_command -> a =
  fun ?(size=Int) fd off cmd ->
    match size with
      | Int -> Unix.lseek fd off cmd
      | Int64 -> Unix.LargeFile.lseek fd off cmd
;;
(*
 * fun ?(size=Int) fd off cmd ->
 *            ^^^
 * Error: This expression has type int size
 *        but an expression was expected of type a size
*)

Is there a way to write this so it types correctly? I guess I would need
to somehow specify a default type for "a" for the "a size" argument to
be optional.

MfG
        Goswin