Can't write a transition which can lead to two different states

Learning
1

Hi,

I heard that, in OCaml, GADTs is the best way to write a statically typesafe explicit state machine, especially because it allows to write exhaustive pattern matching without referencing all the constructors of the type representing the states. For instance i have this code :

type _ state = 
  | Readable : in_channel -> [`Readable] state
  | Eof : in_channel -> [`Eof] state
  | Closed : in_channel -> [`Closed] state
      
let open_file path = Readable (open_in path)
let read_line state = match state with
  | Readable in_c -> 
    try 
      let _ = input_line in_c in
      Readable in_c
    with
    End_of_file -> Eof inc_c

Which is an attempt of representing a simple state machine for file management, and naively i wanted my transition read_line being able to return a Readable or a Eof state, but i get this error when trying :

This expression has type [ Eof ] state but an expression was expected of type [ Readable ] state
These two variant types have no intersection

Which i’m not sure to fully understand, even if i guess that i get this error for the same reason that i can write an exhaustive pattern matching like the one in open_file function

How can i achieve that ? Is this even possible with GADT ? Is this idiomatic ? Any kind of feedback is welcome.

2

The reason why the compiler is complaining about the types having no intersection is because you’ve imposed closed constraints on your state type. If you change state to be

type _ state = 
  | Readable : in_channel -> [> `Readable] state
  | Eof : in_channel -> [> `Eof] state
  | Closed : in_channel -> [> `Closed] state

(and fix the typo in of inc_c → in_c) your code compiles fine. There’s some information in the manual in case you haven’t seen that syntax before.

However the GADT isn’t really getting you much here. If you want to model the function being able to return multiple states, you could just return in_channel * [ `Readable | `Closed ] (this does mean you have to carry around your in_channel separately though).

1 Like
3

Thank you for your help, however, using your fix or only polymorphic variant leads to a problem I wanted to avoid :

now the pattern matching in my function read_line isn’t exhaustive anymore so it’s not the same state machine, I want my read_line function to be defined only for the Readable state, statically I mean.

(Or maybe I’m missing something)

4

@dinosaure has a great blog post about using GADTs for state machines that you might find helpful.

1 Like
6

An important point to keep in mind is that even with GADTs, OCaml is not dependently typed: types cannot depend of the content of a value or the result of a computation.

Your transition

    try 
      let _ = input_line in_c in
      Readable in_c
    with
    End_of_file -> Eof inc_c

doesn’t satisfy this contraint since the final state depends of the result of a runtime computation.

In this case, the fix might be to simply acknowledge that the two branches of the code are different:

match input_line ic_c with
| c -> Ok (Readable in_c)
| exception End_of_file -> Error (Eof inc_c)

However, it is indeed quite common that when interacting with the external world one might need to have a type that represent an unknown state:

type any_state = Any: 'a state -> any_state [@@unboxed]

which could also be used in this context (while losing the information the Closed case is missing):

match input_line ic_c with
| c -> Any (Readable in_c)
| exception End_of_file -> Any (Eof inc_c)

If you had static transitions, another more complex possibility would have been to represent the transitions in the type itself. For instance, we can encode the regexp 0(1)*0 as

type zero_many_one_zero =
  <zero: [`Next of 'many_one]; one: [`No ] >
  constraint
    'many_one = <zero: [`Next of 'stop]; one: [`Next of 'many_one] >
  constraint
    'stop = <zero: [`No]; one: [`No] >

and use this state machine to define a list of Zero and One that necessarily fits this pattern

type ('before,'after) action =
  | One: (<one:[`Next of 'a]; ..>, 'a) action
  | Zero: (<zero:[`Next of 'a]; .. >, 'a) action

type _ trace =
  | []: zero_many_one_zero trace
  | (::): ('before,'after) action * 'before trace ->  'after trace

which we can check with

let ok = [ One; One; Zero ]
let ok2 = [ Zero; One; One; Zero ]
let error = [ One ]
let error2 = [ One; Zero; One; Zero ]
3 Likes
7

Ok i understand now why i can’t do it like i was trying to ! I will pick the first fix you proposed as i think thats the most reasonable, thank you.

8

You should also check this little project which show you how to keep “a state” at the type level with pre/post-condition :slightly_smiling_face: