From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q2PN2UDA018599
	for <caml-list@sympa-roc.inria.fr>; Mon, 26 Mar 2012 01:02:30 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AkQCAHmjb0/ZSMDyjWdsb2JhbABDuCYiAQEBAQkJCwkSBSSCNxN7NAEEKIhCmECfM44EgyQEmz2NOQ
X-IronPort-AV: E=Sophos;i="4.73,648,1325458800"; 
   d="scan'208";a="151142321"
Received: from fmmailgate04.web.de ([217.72.192.242])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 26 Mar 2012 01:02:25 +0200
Received: from moweb001.kundenserver.de (moweb001.kundenserver.de [172.19.20.114])
	by fmmailgate04.web.de (Postfix) with ESMTP id BA56D742C19A
	for <caml-list@inria.fr>; Mon, 26 Mar 2012 01:02:24 +0200 (CEST)
Received: from frosties.localnet ([95.208.118.96]) by smtp.web.de (mrweb002)
 with ESMTPA (Nemesis) id 0LopMx-1SmPGt2m3n-00gmpZ; Mon, 26 Mar 2012 01:02:24
 +0200
Received: from mrvn by frosties.localnet with local (Exim 4.77)
	(envelope-from <goswin-v-b@web.de>)
	id 1SBwS8-0007Ks-7B
	for caml-list@inria.fr; Mon, 26 Mar 2012 01:02:24 +0200
From: Goswin von Brederlow <goswin-v-b@web.de>
To: caml-list@inria.fr
Date: Mon, 26 Mar 2012 01:02:24 +0200
Message-ID: <87y5qouvwf.fsf@frosties.localnet>
User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE)
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Provags-ID:  V02:K0:0MFmczUdLJmh9TnjCwt7NSxAyuzuEUuiMV9KrFUjxnI
 AS4EYXu0YNk3F83HUmpK0qBW0aP0iZ8shkVZCLRkxP2f1e0BKy
 KeWy5733f3dhmnx1MUdLDdX8y3qR5tU2SmrhnFo9gNQL6DIxhh
 DLacfL+59p8DtIuasvnR0ZjBAweK7IbKRi/qcitnlJRCB9UOp+
 QlnnooJXZgA38JKvYbnuQ==
Subject: [Caml-list] GADT and optional arguments: Can they work?

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