Create Presentation
Download Presentation

Download Presentation
## Recursive Type Generativity

- - - - - - - - - - - - - - - - - - - - - - - - - - - E N D - - - - - - - - - - - - - - - - - - - - - - - - - - -

**Recursive Type Generativity**Derek Dreyer Toyota Technological Institute at Chicago ICFP 2005 Tallinn, Estonia**Why Recursive Modules?**• Commonly requested extension to ML • Two major categories of motivating examples: • Splitting up mutually recursive functions and datatypes into separate modules • Encoding certain kinds of data structures that are mutually recursive with a functor application • We’ll see examples of both of these shortly**Recursive ADTs**• What are “Recursive ADTs”? • Want to define two ADTs X and Y, whose implementations are recursive with each other,and also abstract from each other • Modules ¼ ADTs • Recursive modules ¼ Recursive ADTs**The Problem**• Semantics of Recursive ADTs not well understood • Not possible to express them in System F (+ recursion) • Goal of this work: Study and remedy this problem at the level of System F • This is a prerequisite for understanding semantics of recursive modules.**Overview**• Motivating examples • High-level description of my approach • Separate compilation and other issues • Related work and conclusion**GUI-Widget Example**• Both interfaces refer to both abstract types. • GUI specifies operations that are privy to the implementation of the gui type, but not of the wid type. • WID specifies operations that are privy to the implementation of the wid type, but not of the gui type.**Abstraction Before the Fact: Hard**• Existing approaches sidestep the issue: • E.g. in Moscow ML, the gui and wid type representations would need to be visible to both gui_adt and wid_adt Not in scope**Problem**We need heap_typ up here... ...but it only comes into scope down here.**Applicative Solution**• Can avoid this problem by using applicative functors. • This doesn’t help us if we are given a MkHeap with the generative type (as is the case in SML). • Are applicative functors really a prerequisite of recursive ADT’s? • Even if they were, this still wouldn’t help us with the GUI-Widget example.**Overview**• Motivating examples • High-level description of my approach • Separate compilation and other issues • Related work and conclusion**Key Idea**• Problem in both examples is that we want to refer to an ADT before its definition has been given. • So: The key idea is to allow abstract data types to be “created” before their definitions are given. • This is analogous to the idea of recursive backpatching (aka value recursion), but at the type level instead of the term level.**Bootstrapped Heap Encoding**• First, introduce fresh abstract types that are as yet undefined.**Bootstrapped Heap Encoding**• Now we can define boot_typ in terms of heap_typ because heap_typ is in scope.**Bootstrapped Heap Encoding**• The unpacking gives us a fresh type heap_typ’.**Bootstrapped Heap Encoding**• Finally, we can backpatch the definition for heap_typ.**Overview**• Motivating examples • High-level description of my approach • Separate compilation and other issues • Related work and conclusion**Separate Compilation**• What if we want to compile the GUI and Widget implementations separately?**Another Form of Universal**• To support separate compilation, we allow parameterization over undefined var’s (" K).**Recursive Linking**• Now we can link the ADTs recursively.**Rest of the Paper**• Type and effect system: ; ` e : A [] • Avoiding type cycles • We avoid equi-recursive types via ML-style division intotransparent “type” definitions ( := A) andopaque “datatype” definitions ( :¼ A). • Encoding of existential types in “destination-passing style” • || 9: K. A ||DPS = 8" K. unit A**Related Work**• Main related work is Flatt and Felleisen’s units. • Intended as modules for Scheme, but [FF98] also show how to support abstract type components in modules. • Type system allows recursive definitions of ADT’s. • But unit constructs are somewhat heavy and awkward. • As a result, ML module system folks have ignored it as a strange zoo animal, but we shouldn’t. • In some sense, I have given a simpler, cleaner way of accounting for the “good” ideas of units, which fits in better with the traditional account of ADT’s.**Future Work**• Defining a recursive module extension to ML by translation into this calculus • Combining with other improvements to ML module system • This approach is very operational. Can we develop any semantic model or prove any interesting abstraction theorems?