An Effectful Way to Eliminate Addiction to Dependence

Pierre-Marie Pédrot 1, 2, 3 Nicolas Tabareau 3, 2
3 ASCOLA - Aspect and Composition Languages
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
Abstract : We define a monadic translation of type theory, called weaning translation, that allows for a large range of effects in dependent type theory—such as exceptions, non-termination, non-determinism or writing operation. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions (CIC) with a restricted version of dependent elimination. Finally, we show how to recover a translation of full CIC by mixing parametricity techniques with the weaning translation. This provides the first effectful version of CIC.
Type de document :
Pré-publication, Document de travail
2017
Liste complète des métadonnées

https://hal.inria.fr/hal-01441829
Contributeur : Nicolas Tabareau <>
Soumis le : vendredi 20 janvier 2017 - 11:20:25
Dernière modification le : jeudi 15 juin 2017 - 09:08:56

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01441829, version 1

Collections

Citation

Pierre-Marie Pédrot, Nicolas Tabareau. An Effectful Way to Eliminate Addiction to Dependence. 2017. <hal-01441829>

Partager

Métriques

Consultations de
la notice

325

Téléchargements du document

221