From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <Tiphaine.Turpin@irisa.fr>
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by yquem.inria.fr (Postfix) with ESMTP id 006A9BBAF
	for <caml-list@yquem.inria.fr>; Sun, 31 Jan 2010 20:31:45 +0100 (CET)
X-IronPort-AV: E=Sophos;i="4.49,378,1262559600"; 
   d="scan'208";a="50630567"
Received: from 91-163-91-179.rev.libertysurf.net (HELO [192.168.1.2]) ([91.163.91.179])
  by mail1-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 31 Jan 2010 20:31:45 +0100
Message-ID: <4B65D9D4.4030101@irisa.fr>
Date: Sun, 31 Jan 2010 20:28:20 +0100
From: Tiphaine Turpin <Tiphaine.Turpin@irisa.fr>
User-Agent: Thunderbird 2.0.0.19 (X11/20090216)
MIME-Version: 1.0
To: Goswin von Brederlow <goswin-v-b@web.de>
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Problem correlating input and output type
References: <87fx5mi25n.fsf@frosties.localdomain>
In-Reply-To: <87fx5mi25n.fsf@frosties.localdomain>
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Spam: no; 0.00; irisa:01 callbacks:01 runtime:01 sig:01 'foo:01 val:01 val:01 foo:01 'foo:01 struct:01 foo:01 bool:01 bool:01 sig:01 struct:01 

Goswin von Brederlow a écrit :
> Hi,
>
> last night I had a crazy idea
Definitely :-).

> [...]
>
>
> Can anyone think of a way to express this so that the type system keeps
> track of which callbacks are already connected?
>   
Here is an attempt (with only two "events"). Note that :
- the imperative version cannot prevent connecting a signal more than once
- such types can only represent sets of "parallel" edges of a lattice,
i.e., this doesn't generalises to arbitrary "typestate" properties
- this is just a curiosity, and not a reasonable way of doing such
things. Runtime checking would be much easier (but still a bit hackish).

Tiphaine

module LatticeFun : sig

  type ('foo, 'bar) r
  type t and f

  val make : unit -> (f, f) r
  val set_foo : (f, 'bar) r -> (t, 'bar) r
  val set_bar : ('foo, f) r -> ('foo, t) r
  val use : (t, t) r -> unit

end = struct

  type ('foo, 'bar) r = {foo : bool ; bar : bool}

  type t
  type f = t

  let make () = {foo = false ; bar = false}
  let set_foo x = {x with foo = true}
  let set_bar x = {x with bar = true}
  let use _ = ()

end

module LatticeImp : sig

  type ('foo, 'bar) r
  type t and f

  val make : unit -> (f, f) r
  val set_foo : ('foo, 'bar) r -> (t, 'bar) r
  val set_bar : ('foo, 'bar) r -> ('foo, t) r
  val use : (t, t) r -> unit

end = struct

  (* for some reason, the direct declaration causes a module type error *)
  type r1 = {mutable foo : bool ; mutable bar : bool}
  type ('foo, 'bar) r = r1

  type t
  type f = t

  let make () = {foo = false ; bar = false}
  let set_foo x = x.foo <- true ; x
  let set_bar x = x.bar <- true ; x
  let use _ = ()

end