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 [email protected] #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

Back to top button