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.