Wat zijn generics, hoe zorgt dat ervoor dat je functies niet overal voor hoeft te definieren, wat zijn ornaments, hoe lossen ze welk probleem op.
Mergen en splitten van constructors. Example: Toevoegen van types aan een lambda calculus. (`lit : Exp) wordt dan bijvoorbeeld (`bool : Exp Bool) en (`nat : Exp Nat).
Iets met addLimitingIndex ofzo, die overal een index toevoegt. Misschien algebraic ornaments waarbij de Algebra een Maybe oplevert?
Vraag: Je kan descriptions droppen naar een eenvoudiger soort. Kan je ornaments ook liften naar moeilijkere?
Alleen types van descriptions en ornaments. Gebruik van high-level mutaties zoals addParameter en renameArguments.
Begrip van hoe descriptions eruit zien en het maken van ornaments daarvoor.
Snapt de volledige implementatie van descriptions en ornaments
Topics: Description, algebra/fold, ornament, ornamental algebras, algebraic ornaments, quoting/unquoting
Yakushev, Holdermans, Löh, Jeuring 2009: Generic programming with fixed points for mutually recursive datatypes
Danielsson 2007: A partial formalisation of a dependently typed language as an inductive-recursive family
-------- OUDE OUTLINE
Implementatie van een framework waarmee een significant gedeelte van Agda’s datatypes kunnen worden gequote. Met name nuttig voor metaprogrammeren in Agda. De mogelijkheden van het framework worden beschreven in (2). De gekozen representatie van datatypes wordt toegelicht in (3). Een overzicht van metaprogrammeren met Agda is gegeven in (5). Een aantal details van de implementatie worden uitgelicht in (6).
Implementatie van een framework waarmee we operaties op bestaande Agda datatypes kunnen uitvoeren die resulteren in nieuwe datatypes. De implementatie is volledig binnen Agda en is gebaseerd op de theorie achter ornaments. Voor ons framework hoeven de termination en strict positivity checkers niet te worden uitgeschakeld en we hebben geen set-in-set nodig.
Benoem variaties die we niet gekozen hebben en waarom dan niet. Observaties over closed under fixpoints, mutual recursion ↔ indices, higher-order abstract syntax vs DeBruijn passen hier ook.
Ook iets over sized types..
Discussie voornamelijk verplaatsen naar eind van thesis, omdat de gebruiker eerst wil lezen over ornaments.
Gebruik finite types als een korte introductie voor universes.
In principe zijn de constructors 0, 1 en + redundant, ze kunnen ook met Σ geimplementeerd worden. Op deze manier blijven we dicht bij de oorspronkelijke datatypes. * is first-order en soms makkelijker te gebruiken dan Σ (als je geen dependent types nodig hebt), maar voor consistentie genereerd het systeem altijd Σ’s, daarom is * nu niet geimplementeerd. K is redundant als de Σ met Sets geimplementeerd worden (met ΣK).
Onze descriptions zijn closed onder fixpoints. Benoem de alternatieven. (verschuif naar einddiscussie?)
Quote/quoteTerm/unquote. Macros
Equality kan op vele manieren, maar sowieso moet het isomorf zijn met ≅. Voor functies waar een equality in gestopt wordt is het handig als je op de equality zelf kan pattern matchen (ipv op de losse descriptions). Je kan de equality met *-cong dan ook zien als een view.
Leg uit wat het is. Onze descriptions zijn grotendeels first-order, en de verbinding met echte datatypes is duidelijk. Dit is relevant omdat de gebruiker met deze descriptions moet werken en er ornaments voor moet maken.
In syntactische niveaus opgedeeld (atoms/products/sums). Om omzetbaarheid naar een echt datatype te garanderen.
Hierin wordt ook een universe voor strictly positive inductive types beschreven. Er wordt een natural gebruikt om het aantal variabelen waarnaar verwezen wordt te specificeren, en er kan maar één datatype tegelijk worden beschreven. Hun universe correspondeert met ‘IODesc (Fin n) ⊤’ waarbij de fixpoint ‘IOFunc (Fin (suc n)) ⊤ → IOFunc (Fin n) ⊤’ i. Het toepassen van een telescope daar is vergelijkbaar met het toepassen van een (of meer??) request functions.
Vanuit een theoretisch oogpunt is het mooi om geen verwijzingen naar Set te hebben, maar enkel naar descriptions. Sommigen hebben beargumenteerd dat je door het toevoegen van arbitraire Sets geen decidable equality e.d. hebt (Morris 2007, Löh 2011). Wij hebben dat niet nodig en hebben geen praktische bezwaren hiertegen. Het voornaamste alternatief voor verwijzingen naar Set is om iso te gebruiken, daarmee is het mogelijk om descriptions te interpreteren als het native type waarmee ze corresponderen, waarmee ze significant makkelijker worden om te gebruiken in Σ (dependent types, geef voorbeeld). De interpretatie van iso geeft echter problemen met de termination checker (mailing list).
data Prompt (A : Set) : String → Set ret : a → Prompt A s Of bijv
Makkelijkere manieren om ornaments te bouwen, voor mensen die geen kennis hebben van descriptions.. insertArg insertParameter type (true ∷ true ∷ []) front ..
Je kan descriptions droppen naar een eenvoudiger soort. Kan je ornaments ook liften naar moeilijkere?