Transporting functions across ornaments - Archive ouverte HAL Access content directly
Journal Articles Journal of Functional Programming Year : 2014

Transporting functions across ornaments

(1) , (2)
1
2

Abstract

Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: we can finally write correct-by-construction software. However, this extreme accuracy is also a curse: a datatype is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any attempt to reuse code across similarly structured data. In this article, we capitalise on the structural invariants of datatypes. To do so, we first adapt the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: the user can ask the definition of addition to be lifted to lists and she will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in a type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.
Fichier principal
Vignette du fichier
paper_colour.pdf (518.22 Ko) Télécharger le fichier
Vignette du fichier
FunOrn/Example.agda (2.28 Ko) Télécharger le fichier
Vignette du fichier
FunOrn/Functions.agda (533 B) Télécharger le fichier
Vignette du fichier
FunOrn/Functions/Examples/Le.agda (1.56 Ko) Télécharger le fichier
Vignette du fichier
FunOrn/Functions/Examples/Plus.agda (1.2 Ko) Télécharger le fichier
Vignette du fichier
FunOrn/FunOrnament.agda (1.65 Ko) Télécharger le fichier
Vignette du fichier
FunOrn/FunOrnament/Examples/Append.agda (472 B) Télécharger le fichier
Vignette du fichier
FunOrn/FunOrnament/Examples/Lookup.agda (545 B) Télécharger le fichier
Vignette du fichier
FunOrn/Lift/Case.agda (992 B) Télécharger le fichier
Vignette du fichier
FunOrn/Lift/Constructor.agda (886 B) Télécharger le fichier
Vignette du fichier
FunOrn/Lift/Examples/Append.agda (1.63 Ko) Télécharger le fichier
Vignette du fichier
FunOrn/Lift/Examples/Head.agda (1.48 Ko) Télécharger le fichier
Vignette du fichier
FunOrn/Lift/Examples/Lookup.agda (2.63 Ko) Télécharger le fichier
Vignette du fichier
FunOrn/Lift/Fold.agda (952 B) Télécharger le fichier
Vignette du fichier
FunOrn/Lift/Induction.agda (984 B) Télécharger le fichier
Vignette du fichier
FunOrn/Lift/MkReorn.agda (2.97 Ko) Télécharger le fichier
Vignette du fichier
FunOrn/Patch.agda (628 B) Télécharger le fichier
Vignette du fichier
FunOrn/Patch/Apply.agda (795 B) Télécharger le fichier
Vignette du fichier
FunOrn/Patch/Coherence.agda (992 B) Télécharger le fichier
Vignette du fichier
FunOrn/Patch/Examples/Append.agda (265 B) Télécharger le fichier
Vignette du fichier
FunOrn/Patch/Examples/Lookup.agda (264 B) Télécharger le fichier
Vignette du fichier
html/Agda.css (1.19 Ko) Télécharger le fichier
Vignette du fichier
html/Agda.Primitive.html (7.16 Ko) Télécharger le fichier
Vignette du fichier
html/Algebra.FunctionProperties.Core.html (6.33 Ko) Télécharger le fichier
Vignette du fichier
html/Algebra.FunctionProperties.html (59.73 Ko) Télécharger le fichier
Vignette du fichier
html/Algebra.html (154.67 Ko) Télécharger le fichier
Vignette du fichier
html/Algebra.Structures.html (209.33 Ko) Télécharger le fichier
Vignette du fichier
html/Category.Applicative.html (7.19 Ko) Télécharger le fichier
Vignette du fichier
html/Category.Applicative.Indexed.html (59.78 Ko) Télécharger le fichier
Vignette du fichier
html/Category.Functor.html (8.06 Ko) Télécharger le fichier
Vignette du fichier
html/Category.Monad.html (16.95 Ko) Télécharger le fichier
Vignette du fichier
html/Category.Monad.Identity.html (6.18 Ko) Télécharger le fichier
Vignette du fichier
html/Category.Monad.Indexed.html (35.06 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Bool.html (24.69 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Empty.html (4.22 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Fin.html (115.77 Ko) Télécharger le fichier
Vignette du fichier
html/Data.List.html (213.67 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Maybe.Core.html (4.98 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Maybe.html (119.1 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Nat.html (122.89 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Product.html (94.16 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Sum.html (36.66 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Unit.Core.html (12.14 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Unit.html (21.71 Ko) Télécharger le fichier
Vignette du fichier
html/Data.Vec.html (203.24 Ko) Télécharger le fichier
Vignette du fichier
html/Function.Equality.html (56.27 Ko) Télécharger le fichier
Vignette du fichier
html/Function.Equivalence.html (65.35 Ko) Télécharger le fichier
Vignette du fichier
html/Function.html (69.75 Ko) Télécharger le fichier
Vignette du fichier
html/Function.Injection.html (29.57 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Example.html (53.97 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Functions.Examples.Le.html (32.43 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Functions.Examples.Plus.html (29.68 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Functions.html (11.96 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.FunOrnament.Examples.Append.html (7.14 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.FunOrnament.Examples.Lookup.html (7.74 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.FunOrnament.html (33.09 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Lift.Case.html (19.6 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Lift.Constructor.html (16.32 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Lift.Examples.Append.html (30.49 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Lift.Examples.Head.html (30.79 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Lift.Examples.Lookup.html (55.61 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Lift.Fold.html (18.5 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Lift.Induction.html (19.72 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Lift.MkReorn.html (82.42 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Patch.Apply.html (14.41 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Patch.Coherence.html (16.48 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Patch.Examples.Append.html (3.28 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Patch.Examples.Lookup.html (3.28 Ko) Télécharger le fichier
Vignette du fichier
html/FunOrn.Patch.html (13.86 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Case.html (10.63 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.Bool.html (9.09 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.Expr.html (32.94 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.Fin.html (27.7 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.Forest.html (20.15 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.Id.html (8.77 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.List.html (12.68 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.Nat.html (11.9 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.Ordinal.html (13.64 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.STLC.html (41.58 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.Vec.html (31.87 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Examples.Walk.html (16.67 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Fixpoint.html (4.13 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.IDesc.html (46.46 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Induction.html (24.24 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.InitialAlgebra.html (24.1 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Lifting.html (40.2 Ko) Télécharger le fichier
Vignette du fichier
html/IDesc.Tagged.html (30.05 Ko) Télécharger le fichier
Vignette du fichier
html/Level.html (5.16 Ko) Télécharger le fichier
Vignette du fichier
html/Logic.IProp.html (36.64 Ko) Télécharger le fichier
Vignette du fichier
html/Logic.Logic.html (7.79 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.AlgebraicOrnament.Coherence.html (75.92 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.AlgebraicOrnament.Examples.Expr.html (57.87 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.AlgebraicOrnament.Examples.Leq.html (27.27 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.AlgebraicOrnament.Examples.Lifting.html (8.6 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.AlgebraicOrnament.Examples.Vec.html (14.3 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.AlgebraicOrnament.html (20.74 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.AlgebraicOrnament.Make.html (97.19 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Brady.Fin.html (18.25 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Brady.Vec.html (16.93 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Ornament.Algebra.html (12.06 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Ornament.CartesianMorphism.html (29.18 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Ornament.Examples.Fin.html (32.56 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Ornament.Examples.Lifting.html (19.95 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Ornament.Examples.List.html (16.12 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Ornament.Examples.Maybe.html (15.43 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Ornament.Examples.Vec.html (36.07 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Ornament.html (49.43 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Ornament.Identity.html (13.51 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Reornament.Algebra.html (13.56 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Reornament.Coherence.html (70.43 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Reornament.Examples.Iterative.html (56.06 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Reornament.Examples.List.html (8.85 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Reornament.Examples.Maybe.html (7.95 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Reornament.html (36.77 Ko) Télécharger le fichier
Vignette du fichier
html/Orn.Reornament.Make.html (32 Ko) Télécharger le fichier
Vignette du fichier
html/Readme.html (24.32 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.Consequences.Core.html (10.63 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.Consequences.html (87.01 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.Core.html (131.39 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.EqReasoning.html (6.72 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.HeterogeneousEquality.Core.html (9.51 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.html (139.41 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.Indexed.Core.html (39.99 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.Indexed.html (15.43 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.PartialOrderReasoning.html (4.61 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.PreorderReasoning.html (22.82 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.PropositionalEquality.Core.html (17 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.PropositionalEquality.html (112.79 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Binary.PropositionalEquality.TrustMe.html (7.13 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Nullary.Core.html (7.48 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Nullary.Decidable.html (65.54 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Nullary.html (3.62 Ko) Télécharger le fichier
Vignette du fichier
html/Relation.Unary.html (68.64 Ko) Télécharger le fichier
Vignette du fichier
IDesc/Case.agda (471 B) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Bool.agda (480 B) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Expr.agda (1.38 Ko) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Fin.agda (1.41 Ko) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Forest.agda (1022 B) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Id.agda (486 B) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Lifting.agda (2.35 Ko) Télécharger le fichier
Vignette du fichier
IDesc/Examples/List.agda (625 B) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Nat.agda (641 B) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Ordinal.agda (664 B) Télécharger le fichier
Vignette du fichier
IDesc/Examples/STLC.agda (1.6 Ko) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Vec.agda (1.56 Ko) Télécharger le fichier
Vignette du fichier
IDesc/Examples/Walk.agda (745 B) Télécharger le fichier
Vignette du fichier
IDesc/Fixpoint.agda (164 B) Télécharger le fichier
Vignette du fichier
IDesc/IDesc.agda (1.9 Ko) Télécharger le fichier
Vignette du fichier
IDesc/Induction.agda (945 B) Télécharger le fichier
Vignette du fichier
IDesc/InitialAlgebra.agda (901 B) Télécharger le fichier
Vignette du fichier
IDesc/Lifting.agda (1.24 Ko) Télécharger le fichier
Vignette du fichier
IDesc/Tagged.agda (1.19 Ko) Télécharger le fichier
Vignette du fichier
Logic/IProp.agda (2.57 Ko) Télécharger le fichier
Vignette du fichier
Logic/Logic.agda (296 B) Télécharger le fichier
Vignette du fichier
Orn/Algebra/VerticalComposition.agda (1.23 Ko) Télécharger le fichier
Vignette du fichier
Orn/AlgebraicOrnament.agda (1.08 Ko) Télécharger le fichier
Vignette du fichier
Orn/AlgebraicOrnament/Coherence.agda (3.35 Ko) Télécharger le fichier
Vignette du fichier
Orn/AlgebraicOrnament/Examples/Expr.agda (2.16 Ko) Télécharger le fichier
Vignette du fichier
Orn/AlgebraicOrnament/Examples/Fin.agda (1.47 Ko) Télécharger le fichier
Vignette du fichier
Orn/AlgebraicOrnament/Examples/Leq.agda (1.22 Ko) Télécharger le fichier
Vignette du fichier
Orn/AlgebraicOrnament/Examples/Lifting.agda (572 B) Télécharger le fichier
Vignette du fichier
Orn/AlgebraicOrnament/Examples/Vec.agda (793 B) Télécharger le fichier
Vignette du fichier
Orn/AlgebraicOrnament/Make.agda (4.1 Ko) Télécharger le fichier
Vignette du fichier
Orn/Brady/Fin.agda (1.02 Ko) Télécharger le fichier
Vignette du fichier
Orn/Brady/Vec.agda (1.1 Ko) Télécharger le fichier
Vignette du fichier
Orn/Ornament.agda (2.09 Ko) Télécharger le fichier
Vignette du fichier
Orn/Ornament/Algebra.agda (683 B) Télécharger le fichier
Vignette du fichier
Orn/Ornament/CartesianMorphism.agda (1.18 Ko) Télécharger le fichier
Vignette du fichier
Orn/Ornament/Examples/Fin.agda (1.61 Ko) Télécharger le fichier
Vignette du fichier
Orn/Ornament/Examples/Lifting.agda (681 B) Télécharger le fichier
Vignette du fichier
Orn/Ornament/Examples/List.agda (832 B) Télécharger le fichier
Vignette du fichier
Orn/Ornament/Examples/Maybe.agda (935 B) Télécharger le fichier
Vignette du fichier
Orn/Ornament/Examples/Vec.agda (1.73 Ko) Télécharger le fichier
Vignette du fichier
Orn/Ornament/Identity.agda (571 B) Télécharger le fichier
Vignette du fichier
Orn/Reornament.agda (1.44 Ko) Télécharger le fichier
Vignette du fichier
Orn/Reornament/Algebra.agda (699 B) Télécharger le fichier
Vignette du fichier
Orn/Reornament/CartesianMorphism.agda (1.13 Ko) Télécharger le fichier
Vignette du fichier
Orn/Reornament/Coherence.agda (2.99 Ko) Télécharger le fichier
Vignette du fichier
Orn/Reornament/Examples/Iterative.agda (2.99 Ko) Télécharger le fichier
Vignette du fichier
Orn/Reornament/Examples/List.agda (459 B) Télécharger le fichier
Vignette du fichier
Orn/Reornament/Examples/Maybe.agda (462 B) Télécharger le fichier
Vignette du fichier
Orn/Reornament/Make.agda (1.39 Ko) Télécharger le fichier
Vignette du fichier
Orn/Reornament/OrnamentalAlgebra.agda (617 B) Télécharger le fichier
Vignette du fichier
paper_bw.pdf (503.63 Ko) Télécharger le fichier
Vignette du fichier
Readme.agda (3.55 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Origin : Files produced by the author(s)
Format : Other
Loading...

Dates and versions

hal-00922581 , version 1 (28-12-2013)

Identifiers

Cite

Pierre-Évariste  Dagand, Conor  Mcbride. Transporting functions across ornaments. Journal of Functional Programming, 2014, 24 (2-3), pp.67. ⟨10.1017/S0956796814000069⟩. ⟨hal-00922581⟩

Collections

INRIA INRIA2
196 View
378 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More