Prohibiting invalid states with GADT - the airlock exercise

Community
21

Currently, the close function return the close type (as a post-condition). So, statically it assumes that your computation close properly the file descriptor. Afterthat, you can compute a specialized version of a computation which terminates by the close post-condition.

However, if you want to compute any computation (like what run does), you can result with any state. Sage.Refl helps you to introspect the type and prove the equality with Sage.close (note that a PR is pending into ocaml/ocaml to add the Refl constructor into the standard library).

About multiple opened files, it’s currently not possible to do that but it’s probably possible to solve this issue with a tuple of opened file-descriptors.

22

How is this not an infinite loop?

23

Because Create_state is the bottom type? Or how to say it. It’s nil. The end. :slight_smile:

24

This phantom types approach would be a fun exercise to do a typed Forth embedded DSL in OCaml. :slight_smile: The phantom types mirror the stack.

25

Yeah, you’re rigth. I read the code wrong while lying in the bed :smile:

26

The example looks wrong to me too. I would expect the type to include both the starting and ending states, e.g.

module File : sig
  type ('a, 's1, 's2) t
  (** An operation that returns an 'a,
      moving from state 's1 to 's2 *)

  val bind : ('a, 's1, 's2) t -> ('a -> ('b, 's2, 's3) t) -> ('b, 's1, 's3) t

  val close : (unit, open_st, close_st) t