Of Zippers and types

Florian Angeletti
Inria Paris, Chameau sur le Plateau, 7 Janvier 2020 

$ ls
a.ml
b.ml
c.ml
d.ml

  • Discovering project structure
  • Building project

A.ml


module M = struct
  module C = struct
    module D = struct end
  end
end
module type T = B.T
open (M:T)
open C
open D

A.ml

module M = struct
  module C = struct
    module D = struct end
  end
end
module type T = B.T
open (M:T)
open C
open D

B.ml

 module type T = sig end

C.ml

 module D = struct end

D.ml

let x = 0
 

type 'a list =
  | []
  | (::): 'a * 'a list


type ('a,'hole) zipper = {left: 'a list ; hole:'hole; right:'a list}


let next z = match z.right with
  | [] -> None
  |  r :: rs ->
    Some { left = z.hole :: z.left; hole=r; right = rs }




let back z = match z.left with
  | [] -> None
  |  l :: ls ->
    Some { left = ls; hole=l; right = z.hole :: z.right }








let fold_step f z = match z.right with
  | [] -> None
  | a :: right ->
     Some { left = a :: z.left; hole = f z.hole a; right }

let fold_left f start l =
  let rec loop z = match fold_step f z with
      | None -> z.hole
      | Some z -> loop z
  in
  loop { left = [] ; hole = start; right = l }









 Algebraic rules for zipper 


Zipper(a + b) = Zipper(a) + Zipper (b)




Zipper(a * b) = Zipper(a) * b + a * Zipper(b)



 


 Deriving a zipper for list 



list(x) = 1 + x * list(x)




Zipper list x = Zipper x * list x + x * Zipper list x





 Direct translation 


type ('a,'h) zipper =
  | End: 'h * 'a list
  | Cons: 'a * 'a zipper





 After simplification 



type 'a zipper = {
  left: 'a list;
  hole:'a;
  right: 'a list;
}










 type 'a t = Leaf of 'a | Node of 'a t * 'a t

























type direction = Left | Right
type 'a zipper = {
  path: (direction * 'a t) list;
  hole: 'a t
}







Zipper t x = Zipper x + (2 * t) * Zipper t x 



type direction = Left | Right
type 'a zipper = { hole: 'a t; path: (direction * 'a t) list }








let left z = match z.hole with
  | Node (l,r) -> Some { hole = l; path = (Right,r) :: z.path }
  | Leaf _ -> None

let right z = match z.hole with
  | Node (l,r) -> Some { hole = r; path = (Left,l) :: z.path }
  | Leaf _ -> None

let up z = match z.path with
  | [] -> None
  | (Left, l) :: path ->
    Some { path; hole = Node(l,z.hole) }
  | (Right, r) :: path ->
    Some { path; hole = Node(z.hole,r) }








type name = string
type 'a expr =
  | Open of 'a
  | Bind_type of name * module_type
  | Bind of name * 'a

and module_ =
 | Structure of module_ expr list
 | Ident of string
 | Constraint of module_ * module_type

and module_type =
  | Signature of module_type expr list
  | Ident of string







type zipper = { hole: hole; path: step list }


and hole =
  | Name of name
  | Module_type of module_type
  | Module of module_
  | Module_expr of module_ expr
  | Module_type_expr of module_type expr



type step =
  | Module_ident
  | Module_type_ident
  | Expr_open
  | Bind_str of string
  | Bind_type_str of name
  | Bind_sig of string
  | Bind_type_sig of name
  | Str of {left:module_ expr list; right:module_ expr list}
  | Sign of {left:module_type expr list; right:module_type expr list}
  | Constraint_left of module_type
  | Constraint_right of module_




exception Stop
let up z = match z.hole, z.path with
  | Name name, Module_ident :: path -> { hole = Module (Ident name); path }
  | Name name, Module_type_ident :: path -> { hole = Module_type (Ident name); path }
  | Module me, Expr_open :: path -> { hole = Module_expr (Open me); path }
  | Module_type mt, Expr_open :: path -> { hole = Module_type_expr (Open mt); path }
  | Module me, Constraint_left mt :: path -> { hole = Module (Constraint(me,mt)); path }
  | Module_type mt, Constraint_right me :: path -> { hole = Module(Constraint(me, mt)); path }
  | Module_expr e, Str {left; right } :: path ->
    { hole = Module(Structure (List.rev_append left (e :: right))); path }
  | Module_type_expr mte, Sign {left; right } :: path ->
    { hole = Module_type(Signature (List.rev_append left (mte :: right))); path }
  | Module m, Bind_str name :: path ->
    { hole = Module_expr(Bind(name,m)); path }
  | Module_type mt, Bind_type_str name :: path ->
    { hole = Module_expr(Bind_type(name,mt)); path }
  | Module_type mt, Bind_sig name :: path ->
    { hole = Module_type_expr(Bind(name,mt)); path }
  | Module_type mt, Bind_type_sig name :: path ->
    { hole = Module_type_expr(Bind_type(name,mt)); path }
  | Module m, [] -> raise Stop
  | _ -> assert false








    

  •  A lot of invalid states  
    • 

      

    •  Path elements can follow any other elements

       let invalid_path = [Module_ident; Module_ident]

      

      • 


    •  The type of the hole is independent of the path 
      • 

       let nonsense = { hole = Structure []; path = [Module_ident] }

      

    

  •  Exhaustiveness checking is impossible 
    • 

  •  Lot of redundancy 
    • 









    

       Two class of types

    •  a zipper type

    •  a familly of path type for each final type of the path 
      • 

    

      
  
    •  A foreign constructor Root 
      • 

    


    type zipper =
  | String_hole of string * to_string
  | Module_expr_hole of module_ expr * to_module_expr
  | Module_type_expr_hole of module_type expr * to_module_type_expr
  | Module_hole of module_ * to_module
  | Module_type_hole of module_type * to_module_type

    




    and to_string =
  | Module_Ident of to_module
  | Module_type_ident of to_module_type

and to_module_type =
  | Expr_open of to_module_type_expr
  | Constraint of {data: module_; prev: to_module}
  | Bind of {data: string; prev:to_module_expr }
  | Bind_sig of {data: string; prev:to_module_type_expr }

and to_module_expr =
  | Structure of {left: module_ expr list; prev: to_module; right: module_ expr list}

and to_module_type_expr =
  | Signature of {left: module_type expr list; prev: to_module_type; right: module_type expr list}

and to_module =
  | Root

  | Expr_open of to_module_expr
  | Constraint of {data:module_type; prev:to_module}
  | Bind of {data: string; prev:to_module_expr }
  | Bind_sig of {data: string; prev:to_module_type_expr }

    
    




      exception Stop
  let up = function
    | String_hole (s, prev) ->
      begin match prev with
        | Module_Ident prev -> Module_hole(Ident s, prev)
        | Module_type_ident prev -> Module_type_hole(Ident s, prev)
      end
    | Module_expr_hole (m, Structure {left; right; prev}) ->
      Module_hole (Structure (List.rev_append left (m::right)), prev)
    | Module_type_expr_hole (m, Signature {left; right; prev}) ->
      Module_type_hole (Signature (List.rev_append left (m::right)), prev)
    | Module_hole (m, prev) ->
      begin match prev with
        | Root -> raise Stop
        | Expr_open prev -> Module_expr_hole(Open m, prev)
        | Constraint {data; prev} -> Module_hole(Constraint(m,data), prev)
        | Bind {data; prev} -> Module_expr_hole(Bind(data,m),prev)
        | Bind_sig {data; prev} -> Module_type_expr_hole(Bind(data,m),prev)
      end
    | Module_type_hole(mt,prev) ->
      begin match prev with
        | Expr_open prev -> Module_type_expr_hole(Open mt, prev)
        | Constraint {data; prev} -> Module_hole(Constraint(data,mt), prev)
        | Bind {data; prev} -> Module_expr_hole(Bind_type(data,mt),prev)
        | Bind_sig {data; prev} -> Module_type_expr_hole(Bind_type(data,mt),prev)
      end

    

    



      

    •  Still some redundancy 
      • 

    •  Nested matches 
      • 

    •  The list of element is hidden 
      • 

    
    




     Can we get back to a tree zipper as a list of unvisited subtrees ?
    


    type ('a,'b) zipper = { hole:'a; path:('a,'b) path }

    

    and ('a,'b) path =
  | []: ('a,'a) path
  | (::): ('a,'b) step * ('b,'c) path -> ('a,'c) path

    


    and (_,_) step =
  | Module_Ident: (string, module_) step
  | Module_type_ident: (string, module_type) step
  | Expr_open: ('a, 'a expr) step
  | Constraint_left: module_type -> (module_,module_) step
  | Constraint_right: module_ -> (module_type, module_) step
  | Str: { left: module_ expr list; right:module_ expr list } ->
      (module_ expr, module_) step
  | Sign: { left: module_type expr list; right:module_type expr list } ->
      (module_type expr, module_type) step
  | Bind_str:string -> (module_, module_ expr) step
  | Bind_sig:string -> (module_, module_type expr) step
  | Bind_type_str:string -> (module_type, module_ expr) step
  | Bind_type_sig:string -> (module_type, module_type expr) step

    


    type 'b any = Any: ('a,'b) zipper -> 'b any

    
    



    

     Only valid paths can be constructed 
    

    let valid = [ Module_ident; Bind_str "M"; Str {left=[];right=[]} ]
let invalid = [ Module_ident; Module_ident ]
                              ^^^^^^^^^^^^
Error: This expression has type (string, module_) step
  but an expression was expected of type (module_, 'a) step
  Type string is not compatible with type module_

    

    

    

     Only valid zippers too 
    

    let valid = { hole = "A"; path = [Module_ident]
let invalid = { hole = "A"; path =  [Bind_str "B"] }
                                     ^^^^^^^^^^^^
Error: This expression has type (module_, module_ expr) step
       but an expression was expected of type (string, 'a) step
       Type module_ is not compatible with type string

    
    




    let up (type b) (Any z: b any): b any  = match z.path with
  | Module_Ident :: path -> Any { hole = Ident z.hole; path }
  | Module_type_ident :: path -> Any { hole = (Ident z.hole:module_type); path }
  | Expr_open :: path -> Any { hole = Open z.hole; path }
  | Constraint_left mt :: path -> Any { hole = Constraint(z.hole,mt); path }
  | Constraint_right me :: path -> Any { hole = Constraint(me, z.hole); path }
  | Str {left; right } :: path ->
    Any { hole = Structure (List.rev_append left (z.hole :: right)); path }
  | Sign {left; right } :: path ->
    Any { hole = Signature (List.rev_append left (z.hole :: right)); path }
  | Bind_str name :: path ->
    Any { hole = Bind(name,z.hole); path }
  | Bind_type_str name :: path ->
    Any { hole = Bind_type(name,z.hole); path }
  | Bind_sig name :: path ->
    Any { hole = Bind(name,z.hole); path }
  | Bind_type_sig name :: path ->
    Any { hole = Bind_type(name,z.hole); path }
  | [] -> raise Stop

    

    




      
  
    •  
       Fully typed 
       
      • 
  
    •  
       No redundancies 
       
      • 
  
    •  
       Unnecessary types can be erased with existentials 
       
      • 

    
    



      
  
    •  Ast definition: 80 lines 
      • 
  
    •  Zipper definition: 120-240 lines
  
    •  Fold: 500 lines 
      • 
  
    •  Generic printer: 200 lines 
      • 

    



  
      
    
    • Zipper are an interesting structure for decomposing computation
      • 
    
    •  They may become unwieldy for complex heterogeneous trees 
      • 
    
    •  
         Combining them with GADTs to avoid:
          
      
        •  invalid states 
          • 
      
        •  redundancy 
          •