feml fool 2006

Parameterized Modules for Classes and Extensible Functions: 

Parameterized Modules for Classes and Extensible Functions Keunwoo Lee Craig Chambers University of Washington FOOL/WOOD workshop, Jan. 2006 computational nihilist (grad student) (advisor)

Consider a module…: 

Consider a module… module Lang = { abstract class Expr of {} abstract fun eval:Expr ! Int }

Desideratum 1:Data type extensibility: 

Desideratum 1: Data type extensibility module C = { class Const extends Lang.Expr of {value:Int} extend fun Lang.eval(Const {value=v}) = v } module Lang = { abstract class Expr of {} abstract fun eval:Expr ! Int }

Desideratum 2:Function extensibility: 

Desideratum 2: Function extensibility module P = { fun print:Lang.Expr ! String extend fun print(Lang.Expr) = '' } module Lang = { abstract class Expr of {} abstract fun eval:Expr ! Int } module C = { class Const extends Lang.Expr of {value:Int} extend fun Lang.eval(Const {value=v}) = v }

Desideratum 3:Reusable extensions: 

class Plus extends L.Expr of {left:L.Expr, right:L.Expr} extend fun L.eval(Plus {left, right}) = … Desideratum 3: Reusable extensions module Lang = { abstract class Expr of {} abstract fun eval:Expr ! Int } signature LangSig = sig { abstract class Expr of {} abstract fun eval:Expr ! Int } module MakePlus = (L:LangSig) ! { } module Plus = MakePlus(Lang) module Plus = MakePlus(Lang) (* { class Plus extends Lang.Expr of {left:Lang.Expr, right:Lang.Expr} extend fun Lang.eval(Plus …) … } *) module Lang = { abstract class Expr of {} abstract fun eval:Expr ! Int }

Desideratum 4:Modular typechecking: 

module Plus = MakePlus(Lang) Desideratum 4: Modular typechecking sig { abstract class Expr of {} abstract fun eval:Expr ! Int } : · signature LangSig = sig { abstract class Expr of {} abstract fun eval:Expr ! Int } module MakePlus = (L:LangSig) ! { class Plus extends L.Expr of {left:L.Expr, right:L.Expr} extend fun L.eval(Plus {left, right}) = … } module Lang = { abstract class Expr of {} abstract fun eval:Expr ! Int }

Desiderata summary: 

Desiderata summary Data type extensibility Function extensibility Reusable extensions Modular typechecking

Related work: 

Related work ML module system [MacQueen 84, …, Dreyer+03] No nontrivial extensible datatypes or functions OO module systems: Jiazzi [McDirmid+01], JavaMod [Ancona/Zucca01], etc. Single-dispatch; function extensibility via design pattern OO parameterized classes: Multiple inheritance, mixins [Bracha/Cook90], traits [Schärli+03,etc.] Virtual types [Madsen/Møller-Pedersen89]: gbeta [Ernst01], Scala [Odersky+04], etc. Single-dispatch; function extensibility via design pattern

Previous work: EML[Millstein et al., ICFP'02]: 

Previous work: EML [Millstein et al., ICFP'02] Extensible datatypes/functions, modular typechecking A simple, restrictive parameterized module system Present work: F(EML) extension of EML with much more useful functors

Outline: 

Outline Desiderata Signatures: key issues Solutions Conclusions

MakePlus, revisited: 

module Plus = MakePlus(Lang) MakePlus, revisited sig { abstract class Expr of {} abstract fun eval:Expr ! Int } : · signature LangSig = sig { abstract class Expr of {} abstract fun eval:Expr ! Int } module MakePlus = (L:LangSig) ! { class Plus extends L.Expr of {left:L.Expr, right:L.Expr} extend fun L.eval(Plus {left, right}) = … } module Lang = { abstract class Expr of {} abstract fun eval:Expr ! Int }

A straw man signature calculus: 

A straw man signature calculus Signatures are compatible iff: Exact syntactic match on declarations Width subtyping: freely permit subsumption to 'forget' extra declarations Both inflexible and unsound

Signatures: Key issues: 

Signatures: Key issues sig { abstract class Expr of {} abstract fun eval:Expr ! Int } signature LangSig = sig { abstract class Expr of {} abstract fun eval:Expr ! Int } Signatures constrain: Names and modularization choices · ) alias declarations module Lang' = { alias class Expr = Foo.Exp alias fun eval = Bar.eval }

Signatures: Key issues: 

Signatures: Key issues sig { abstract class Expr extends Object of {} abstract fun eval:Expr ! Int } signature LangSig = sig { abstract class Expr of {} abstract fun eval:Expr ! Int } signature LangSig = sig { abstract class Expr andlt; Object of {} abstract fun eval:Expr ! Int } · Signatures constrain: Names and modularization choices Relationships among declarations/types ) richer relation language

Signatures: Key issues: 

Signatures: Key issues sig { abstract class Expr extends Object of {} abstract fun eval:Expr ! Int abstract fun f:Expr ! String } signature LangSig = sig { abstract class Expr extends Object of {} abstract fun eval:Expr ! Int } ? · Signatures constrain: Names and modularization choices Relationships among declarations/types Extra parts that may be ignored ) width subtyping via sealing

Signatures: Key issues: 

Signatures: Key issues ) alias declarations ) richer relation language ) width subtyping via sealing Signatures constrain: Names and modularization choices Relationships among declarations/types Extra parts that may be ignored

Outline: 

Outline Desiderata Signatures: key issues Solutions Enriched relations Sealing for subsumption Conclusions

Class relations: 

Class relations signature LangSig = sig { abstract class Expr of {} abstract fun eval:Expr ! Int } module Lang = { abstract class Expr of {} abstract fun eval:Expr ! Int } module MakePlus = (L:LangSig) ! { class Plus extends L.Expr of {left:L.Expr, right:L.Expr} extend fun L.eval(Plus {left, right}) = … }

Class relations: 

Class relations signature BOSig = sig { abstract class BinOp extends Lang.Expr of … } module Lang = { abstract class Expr of {} abstract fun eval:Expr ! Int } module MakePlus = (O:BOSig) ! { class Plus extends O.BinOp of … extend fun Lang.eval(Plus …) = … } module B uses Lang = { abstract class BinOp extends Lang.Expr of … } module Comm uses B, Lang = { abstract class BinOp extends B.BinOp of … }

Enriched class relations: 

Enriched class relations C · C' subtyping C andlt; C' strict subtyping C andlt;k C' k-level subtyping C andlt;1 C' ´ C extends C' C andlt;0 C' ´ C = C' C  C' non-aliasing C disjoint C' non-intersection fresh C freshly declared class

Why these relations?: 

Why these relations? Languages with symmetric-best-match dispatch care about inequalities and non-intersection (which is unusual) How does one prove methods unambiguous? fun f:C ! Unit extend fun f(C) = () extend fun f(D) = () C Å D is non-empty, computable, and covered by a case of f (requires ·) D andlt; C C disjoint D

Deriving disjointness: 

Deriving disjointness

Deriving distinctness: 

Deriving distinctness module C = { class Const extends Lang.Expr … } module N = { class Neg extends Lang.Expr … } module X = (A:sig { class Neg where Neg disjoint C.Const, … }) = … How to modularly deduce non-aliasing? module NBad = { alias class Neg = C.Const … }

Enriched class relations: 

Enriched class relations C · C' subtyping C andlt; C' strict subtyping C andlt;k C' k-level subtyping C andlt;1 C' ´ C extends C' C andlt;0 C' ´ C = C' C  C' non-aliasing C disjoint C' non-intersection fresh C freshly declared class

Outline: 

Outline Desiderata Signatures: key issues Solutions Enriched relations Sealing for subsumption Conclusions

Hiding methods:naïve width subtyping fails: 

module M = { fun f:(Object, Object) ! Unit extend fun f(Object, Object) = () extend fun f(Object, Int) = () } module M = { fun f:(Object, Object) ! Unit extend fun f(Object, Object) = () extend fun f(Object, Int) = () } Hiding methods: naïve width subtyping fails sig { fun f:(Object, Object) ! Unit extend fun f(Object, Object) extend fun f(Object, Int) } : signature S = sig { fun f:(Object, Object) ! Unit } · ? module BreakMS = (A:S) ! { class E extends Object extend fun A.f(E, Object) = () } module Bad = BreakMS(M) module Bad = BreakMS(M) (* { class E extends Object extend fun M.f(E, Object) = () } *)

What's going on?: 

What's going on? A signature's visible parts give clients both capabilities to extend, and obligations they incur by so extending Must never hide an obligation while granting the associated capability…

What's going on?: 

module M = { fun f:(#Object, Object) ! Unit extend fun f(Object _, Object _) = () extend fun f(Object _, Int _) = () } What's going on? sig { fun f:(Object, Object) ! Unit extend fun f(Object, Object) extend fun f(Object, Int) } : signature S = sig { fun f:(Object, Object) ! Unit } · ? module BreakMS = (A:S) ! { class E extends Object extend fun A.f(E, Object) = () } module M = { fun f:(Object, Object) ! Unit extend fun f(Object, Object) = () extend fun f(Object, Int) = () } module Bad = BreakMS(M) module Bad = BreakMS(M) (* { class E extends Object extend fun M.f(E, Object) = () } *) Cannot allow both hiding here… …and extension here

open below: 

open below sig { fun f:(Object, Object) ! Unit open below (Object, Object) extend fun f(Object, Object) extend fun f(Object, Int) } (Object, Object) (Object, Int) (Bad.E, Object) (Bad.E, Int) sig { fun f:(Object, Object) ! Unit open below (Object, Object) extend fun f(Object, Int) } ·

open below: 

open below (Object, Object) (Object, Int) (Bad.E, Object) (Bad.E, Int) supertypes of open below type: cases may be hidden here strict subtypes of open below type: clients may add cases here sig { fun f:(Object, Object) ! Unit open below (Object, Object) } · sig { fun f:(Object, Object) ! Unit open below (Object, Object) extend fun f(Object, Object) extend fun f(Object, Int) }

open below: 

open below (Object, Object) (Object, Int) (Bad.E, Object) (Bad.E, Int) strict subtypes of open below type: clients may add cases here supertypes of open below type: cases may be hidden here sig { fun f:(Object, Object) ! Unit open below (Object, Int) } · sig { fun f:(Object, Object) ! Unit open below (Object, Int) extend fun f(Object, Object) extend fun f(Object, Int) } sig { fun f:(Object, Object) ! Unit open below (Object, Int) extend fun f(Object, Object) extend fun f(Object, Int) extend fun f(Object, String) }

open below: 

open below (Object, Object) (Object, Int) (Bad.E, Object) (Bad.E, Int) sig { fun f:(Object, Object) ! Unit open below (Object, Int) } · sig { fun f:(Object, Object) ! Unit open below (Object, Int) extend fun f(Object, Object) extend fun f(Object, Int) } sig { fun f:(Object, Object) ! Unit open below (Object, Object) } any client that extends below (Object, Int) also extends below (Object, Object)

Hiding functions: 

Hiding functions Unsafe to hide an abstract function, and permit concrete extension of class on which that function is abstract Class sigs can be closed: closed class C … denotes class that cannot be extended via this signature Abstract functions can only be hidden when 'owning' class is closed (andamp; non-instantiable)

Outline: 

Outline Desiderata Signatures: key issues Solutions Conclusions

Status: 

Status Implementation Prototype interpreter: handles our examples Formalization Small-step operational semantics Partial soundness proof (via translation to EML) Summary in paper; details/full proof in technical report (forthcoming) and dissertation (forthcoming, somewhat later)

Conclusions: 

Conclusions F(EML) combines extensibility, code reuse, and modular typechecking; key features: Aliases for renaming/remodularization Rich language of declaration/type relations Signature subsumption via selective sealing Future work: Hierarchical checking of modularity obligations for nested modules (relaxed checking) Multiple dispatch + virtual types + (mutual) recursion