An attempt to translate some examples of Typed design pattern for Functional Era

Learning
1

Hi,

Recently i read this paper that i really enjoyed : https://arxiv.org/pdf/2307.07069.pdf

And as the examples relies on Rust features, i’m trying to translate them in OCaml for learning purpose, and i would like to have some feedbacks.

In particular, i took the state machine page 3 and the parallel lists (Two Lists of heterogeneous elements with a Parallel Relation between the elements) page 5. The purpose was to write in OCaml those pattern with the same static guarantees, in particular :

  • make it illegal to use transitions on improper states
  • guarantee the parallel relationship between the two lists, statically

The use cases are : file management, and a kind of a string formatter.

State machine

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 : [`Readable] state) : [< `Readable | `Eof] state = match state with
  | Readable in_c -> 
    try 
      let _ = input_line in_c in
      Readable in_c
    with
    End_of_file -> Eof in_c
         
let close_file (state: [< `Readable | `Eof] state) : [`Closed] state = match state with
    Readable ic | Eof ic -> close_in ic;Closed ic

let _ =
  let data = open_file "log.txt" in
  let rec loop d =
    match read_line d with
      Readable _ as new_d -> loop new_d
    | Eof _ as break -> break
  in
  let eof_state = loop data in
  (* Doesn't compile
  let illegal_use = read_line eof_state in ...
  *)
  let closed_file = close_file eof_state in
  (* Doesn't compile
  let illegal_use = close_file closed_file in illegal_use
  *)
  closed_file

Parallel lists

A little explanation of what i’ve done : I have two types, one that represents the string with holes to fill (a formatList), and I’ve encoded the size of the list in its type, counting only the number of holes, because I want to match this size with the size of the list that contains all the arguments that will fill the holes (an idList)

type z = Z : z
type 'n s = S : 'n -> 'n s 

type _ formatList = 
    FNil : z formatList
  | FVal : string * 'n formatList -> 'n formatList
  | FArg : 'n formatList -> 'n s formatList
      
type ('a,_) idList =
    IdNil : ('a,z) idList
  | IdCons : 'a * ('a,'n) idList -> ('a,'n s) idList
      
let rec format : type n. n formatList -> (string, n) idList -> string = fun fmt args ->
  match fmt, args with
    FNil,IdNil -> ""
  | FVal(v,tl),_ -> v ^ (format tl args)
  | FArg(tl),IdCons(v,vtl) -> v ^ (format tl vtl)

let _main_formatter () =
  let empty_fmt = FNil in
  let one_fmt = FVal("Hello! ",FArg(empty_fmt)) in

  let args = IdCons("world.",IdNil) in
  format one_fmt args
  (*
     Doesn't compile
  
  let too_much_args = IdCons("world.",IdCons("yo"),IdNil)
  format one_fmt too_much_args
  
  let not_enough_args = IdNil
  format one_fmt not_enough_args

  *)
2 Likes