Version française
Home     About     Download     Resources     Contact us    
Browse thread
Problem correlating input and output type
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Tiphaine Turpin <Tiphaine.Turpin@i...>
Subject: Re: [Caml-list] Problem correlating input and output type
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