Skyb0rg

Untitled

Jan 22nd, 2021 (edited)
395
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. (* Here is a basic example of the Moscow ML first-class-modules extension
  2.  * The comments following each declaration denote what the interpreter responds with (modified for readability)
  3.  *)
  4.  
  5. signature MY_SIG = sig
  6.     type t;
  7.     val x : t;
  8.     val print : unit -> unit;
  9. end;
  10. (* signature MY_SIG = ∃t . sig type t = t; val x : t; val print : unit -> unit; end *)
  11. (* Note: Moscow ML represents abstract types as existentials *)
  12.  
  13. structure StructA : MY_SIG where type t = int = struct
  14.     type t = int;
  15.     val x = 12;
  16.     fun print () = TextIO.print "Hello from StructA\n";
  17. end;
  18. (* structure StructA : sig type t = int; val x : t; val print : unit -> unit; end *)
  19.  
  20. structure StructB : MY_SIG where type t = string = struct
  21.     type t = string;
  22.     val x = "foo";
  23.     fun print () = TextIO.print "Hello from StructB\n";
  24. end;
  25. (* structure StructB : sig type t = string; val x : t; val print : unit -> unit; end *)
  26.  
  27. val structA = [ structure StructA as MY_SIG ];
  28. (* val structA : [ MY_SIG ] *)
  29. (* This syntax represents "structure packing".
  30.  *
  31.  *            structure S : SIG
  32.  * --------------------------------------  Structure Packing
  33.  *  Γ ⊢ [ structure S as SIG ] : [ SIG ]
  34.  *)
  35.  
  36. val structB = [ structure StructB as MY_SIG ];
  37. (* val structB : [ MY_SIG ] *)
  38.  
  39. fun print_struct s =
  40.     let structure S as MY_SIG = s
  41.     in  S.print ()
  42.     end;
  43. (* val print_struct : [ MY_SIG ] -> unit *)
  44. (*
  45.  *               Γ ⊢ e : [ SIG ]
  46.  * -------------------------------------------- Structure Unpacking
  47.  *  structure S as SIG = e ⇒ structure S : SIG
  48.  *)
  49.  
  50. fun conditional_print b =
  51.     let structure S as MY_SIG = if b then structA else structB
  52.     in  S.print ()
  53.     end;
  54. (* conditional_print : bool -> unit *)
  55.  
  56. fun get_x_mono s =
  57.     let structure S as MY_SIG where type t = int = s
  58.     in  S.x
  59.     end;
  60. (* val get_x_mono : [ MY_SIG where type t = int ] -> int *)
  61.  
  62. (* First-class modules require annotations for dependent types *)
  63. functor Dependent(structure S : MY_SIG) = struct
  64.     val x = S.x
  65. end;
  66. (* functor Dependent : (structure S : MY_SIG) -> (sig val x : S.t end) *)
  67.  
  68. fun dependent s =
  69.     let structure S as MY_SIG = s
  70.     in  S.x
  71.     end;
  72. (* Type error: Scope violation *)
  73.  
  74. fun dependent s =
  75.     let structure S as MY_SIG where type t = 'a = s
  76.     in  S.x
  77.     end;
  78. (* val 'a dependent : [ MY_SIG where type t = 'a ] -> 'a *)
  79.  
  80.  
RAW Paste Data