AOP with Type Classes by Martine Sulzmann, Meng W ang
19 Slides320.00 KB
AOP with Type Classes by Martine Sulzmann, Meng W ang
Outline Syntax and key idea Shortcoming and solution Transformation of AOP Haskell Light Automatically and manually AOP Mini Haskell CHR Target language (representing type by value) Type directed transformation GADT Coherence (ambiguity) Comparisons
Syntax And Key Idea joinpoints explicit typed type-scoped
Syntax And Key Idea (cont.) expanded chain expression Weaving util Advice body
Syntax And Key Idea (cont) -fglasgow-exts Multi-parameter type classes -fallow-overlapping-instances Default case covers special case Types insert :: forall a. (Advice N1 (a - [a] - [a]), Advice N2 (a - [a] - [a]), Ord a) a - [a] - [a] a Bool I1 & I2’ a Int I1 & I2
Shortcoming User provided type annotation Drop or rewrite Insert :: Ord a a - [a] - [a] Eagerly resolve constrains yields I1’ & I2’ Polymorphic recursive functions Type check failed [[a]] - Bool
Shortcoming And Solution Problem comes from dictionarypassing scheme In the f in the example, compiler could not generate dictionary for Advice N [a] from the one for Advice N a Switch to pass “types” Dispatch based on run-time type information
AOP Haskell Light Still use dictionary-passing scheme Restriction: each joinpoint is not enclosed by a ty pe annotation, advice or instance declaration For each program For each advice Joinpoints Useful Advice: Adv. type func. type
AOP Haskell Light Manually Rewrite (Advising instance) -fallow-undecidable-instances
AOP Haskell Light Manually Rewrite (Advising advice body) -fallow-undecidable-instances
AOP Mini Haskell Type-passing type class resolution str ategy CHR as intermediate record instance Ord a Advice N1 T instance Advice N1 a Advice N1 T Ord a Advice N1 b b / T True
AOP Mini Haskell Target Language
Type Directed Transformation
Type Directed Transformation (cont.)
GADT Might want to use the standard dictionary-passing scheme for the type class part Use type-passing scheme only for translating advice Use GADT to encode types
GADT (cont.) f :: Type a - [a] - Bool f t [] True f t (x:xs) (joinpoint (turn t) (f (TList t))) [xs] where turn :: Type b - Type ([[b]]- Bool) turn t TArrow (TList (TList t)) TBool check ((TList (TList TBool)) TArrow TBool) MatchTT check MatchFF joinpoint :: Type joinpoint t f case (check t) MatchTT - MatchFF - t - t - t of \x - False f data Type a where TList :: Type a - Type [a] TArrow :: Type a - Type b - Type (a- b) TInt :: Type Int
Coherence (Ambiguity) f :: [a] - Bool f False N@advice #f# :: [[Bool]] - Bool \x - True instance Advice N ([[Bool]]- Bool) instance Advice N a main :: Bool main f undefined main (joinpoint N f) undefined main f (undefined :: [[Bool]]) main f (undefined :: [Int])
Comparisons “Advice is type class with default” We claimed, they used Advice dispatching We generate our own (single entry) dictionary They rely on Haskell compiler to generate a single entry dictionary (Light) Type case (Mini) Type-scoped advice We calculate ourselves (rule Adv-An) They rely on the lazy resolution and “best-fit” strategy applied by GHC (Light) Representing types by values (or GADT) (Mini)
Comparisons (cont.) Advice triggering chain expression & expansion (ours) joinpoint N1 (joinpoint N2 f) (theirs) Type annotation We recalculate and rewrite them They reject those changed by advising (Light) Adding type parameters (Mini) Polymorphic recursive functions Ours: not supported Light: unable to handle (reject due to type annotation) Mini: construct corresponding type