Introductie GADTs zijn nuttig voor diverse toepassingen. We willen GADTs toevoegen aan talen, maar observatie: bestaande aanpakken zijn ingewikkeld (forward reference) Research: (algemeen) hoe voegen we met zo min mogelijk mechanismen zoveel mogelijk taalfeatures toe zodanig dat de implementatie orthogonaal, eenvoudig en begrijpbaar is. (specifiek) Stelling: GADTs krijgen we vrijwel kado indien we een taal hebben met mechanismen voor: - qualified types - user-supplied type signatures Oplossing: - voeg equality-constraints als qualifiers toe - gebruik CHRs - pas unificatie-algoritme aan zodat het equality constraints oplevert bij unificatie-failures - dan GADT implementatie kado; alleen een aantal specifieke CHR-regels nodig (welke gebruik maken van het unificatie algoritme) We illustreren deze oplossing door een vertaling te geven van System F met GADTs naar System Fc (zie sectie xxx). Deze vertaalslag is standaard. De subtiliteit zit in de behandeling van qualified types. Het grootste gedeelte hiervan komt kado wanneer er gebruikt gemaakt wordt van CHRs; er hoeven slechts een handje vol CHR-regels toegevoegd te worden (zie sectie yyy). Huidige aanpakken Huidige aanpakken voor het oplossen van GADTs zijn te ingewikkeld. Type systemen die gegeven worden zijn niet standaard. Er worden teveel nieuwe concepten door elkaar geintroduceerd. Dit maakt met moeilijk om te bepalen wat precies nodig is om GADTs te implementeren. Voorbeeld: "Simple unification-based type inference for GADTs" (Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn) * niet-standaard type systeem; maakt gebruik van most general unifier * ingewikkeld -> alternatief: zie sectie 'transformatie schema' Voorbeeld: "A framework for Extended Algebraic Data Types" (Martin Sulzmann, Jeremy Wazny, and Peter J. Stuckey) * de details met betrekking tot het oplossen van equality constraints worden niet gegeven -> alternatief: zie sectie 'CHR implementatie' Daarom noodzakelijk om precies beschreven te hebben wat er nodig is om GADTs aan een taal toe te voegen, met hergebruik van zoveel mogelijk bestaande mechanismen. Vertaling Vertaling van System F naar System Fc. Brontaal is System F met GADTs. Expliciet getypeerd (abstraheren van type inferentie/checken). Similar and for the same reasons as the core language in "Wobbly types: type inference for generalised algebraic data types" Basically System Fa in "System F with Type Equality Coercions" Doeltaal is System Fc in "System F with Type Equality Coercions". Bekende core-taal. Piggy-backen op proofs voor System Fc. Opsommen van wat conventies wat betreft notatie. Introduceren van System F met GADTs. Specifieke uitbreidingen: data-type declarations, recursieve let, case-expression, pattern matches en existentials. Geven van type system voor System F met GADTs. Aspect van existentials (verwijzing naar pierce). Typeren van pattern matches. Signaturen van value constructors (construction en deconstruction). Toevoeging voor gadts: aannamen bij pattern matchen (mechanismen moeten al aanwezig zijn omdat aannamen in geval van qualified types al geintroduceerd moeten worden maar dan door explicite type-signaturen). Bewijsverplichting bij bouwen waarde van value- constructor (overeenkomst met voorkomen van overloaded identifiers). Opmerkingen over syntax-directed en implementatie, zoals: bewijsverplichtingen die door falende unificaties worden opgeleverd. Introduceren van entailment als interface naar constraint-solving. Uitleggen van de zes regels en de noodzaak van deze regels. Introduceren van System Fc. Korte uitleg over de coercions. Noemen dat de coercions waarden van het Equality-data type zijn en erased kunnen worden? Vertaalschema van System F met GADTs naar System Fc. Interessante plaatsen: waar aannamen geintroduceerd worden (pattern matches binden een naam aan evidence) en waar bewijsverplichtingen geintroduceerd worden (daar moet een coercion toegepast worden). De coercions zelf worden gegenereerd door een aangepaste entailment-relatie dat evidence oplevert. The left, right, univ, inst and congruence rule kunnen met een algemene regel geimplementeerd worden. Conclusie dat zodra er mechanismen zijn voor qualified types, dat de hoofdzakelijke aanpassing die voor GADTs gemaakt moet worden is dat de entailment-relatie voor equality-constraints geimplementeerd moet worden. Bewijs dat een welgetypeerde Fa term een welgetypeerde Fc term is. Entailment met CHRs De entailment-relatie kan geimplementeerd worden door er specifiek een algoritme voor te schrijven. Echter, Constraint Handling Rules is een algemeen mechanisme om entailment mee te implementeren. CHR regels voor GADTs. Correspondentie met de entailment relatie in de type regels. Structuur van de regels: guard, reduction (evidence); uitleg van de guards die nodig zijn. Details ook laten zien? Zoals het uitpakken van een rijtje van constraints. Algoritme om deze CHRs op te lossen (CHR-pipeline, gerrit&atze's werk): CHRs + constraints -> reductions -> graph -> evidence CHR+constraints naar reductions. Reductions naar reduction graph. Reduction graph naar GADT evidence. Related work "Type inference and type error diagnosis for Hindly/Milner with extensions" no specific solver for GADTs, complicated solver "Simple unification-based type inference for GADTs" (Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Geoffrey Washburn) "A framework for Extended Algebraic Data Types" (Martin Sulzmann, Jeremy Wazny, and Peter J. Stuckey) "Stratified type inference for generalized algebraic data types." (Franc¸ois Pottier and Yann R´egis-Gianas) "Type inference for guarded recursive data types." (Peter Stuckey and Martin Sulzmann) Conclusion and future work Efficiency genereer CHR regels i.p.v. class constraints Irrefutable patterns References: Arthur L Baars and S. Doaitse Swierstra. Typing dynamic typing. In ACM SIGPLAN International Conference on Functional Programming (ICFP’02), pages 157–166, Pittsburgh, September 2002. ACM. Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich. Wobbly types: type inference for generalised algebraic data types. Microsoft Research, 2004 Franc¸ois Pottier and Yann R´egis-Gianas. Stratified type inference for generalized algebraic data types. In ACM Symposium on Principles of Programming Languages (POPL’06), Charleston, January 2006. ACM. Peter Stuckey and Martin Sulzmann. Type inference for guarded recursive data types. Technical report, National University of Singapore, 2005. Martin Sulzmann, JeremyWazny, and Peter Stuckey. A framework for extended algebraic data types. Technical report, National University of Singapore, 2005. H. Xi, C. Chen, and G. Chen. Guarded recursive datatype constructors. In Proc. of POPL ’03, pages 224–235, New York, NY, USA, 2003. ACM Press.