Notes - typerole

Posted on June 3, 2018

from Generative Type Abstraction and Type-level Computation - weirich vytiniotis spj zdancewic

Motivation personelle

Comment raffiner une theorie en gardant en interne le fait que deux operations doivent etre egales, et en forcant les clients a travailler sans cette egalite. Cette question revient frequemment : on remplace une egalite (qui est une idee platonicienne, existant de toute eternite) par un isomorphisme (qui est une fonction, qui a un nom, qui peut etre passse en argument).

On en voit une autre illustration dans les types de Haskell, ou attribuer des noms differents a des structures identiques force les clients a distinguer et a referencer explicitement des isos pour passer d’un type a un autre.

Nous regardons donc comment c’est traite dans le papier mentionne

Introduction

> newtype Age = MkAge Int
> 
> data K a where
>   KAge :: K Age
>   KInt :: K Int
> 
> cvt ::  c. c Int  c Age
> cvt x = undefined -- identite : an Age is an Int

remarque interessante sur les modules dans ML, ou DANS un module, on Age et Int sont vraiment synonymes.

trouble in paradise

> kint :: K Age
> kint = cvt KInt -- the representation is the same
> 
> get :: K Age  Bool -- only defined at K Age
> get KAge = True     -- so this pattern match is exhaustive

yet this will fail :

> vf = get kint

(flash news : le domaine d’une fonction fait partie de sa definition. fonction identite agit uniformement, mais l’identite en A n’est pas l’identite en B. si les noms ont de l’importance, ca ne passe pas sans preuve que A = B, preuve detenue uniquement en interne par la personne ayant cree le newtype.)

more trouble

> type family F a :: *
> type instance F Age = Char
> type instance F Int = Bool

Permet de deduire :

“What went wrong? Maybe it should be illegal for a type function to behave differently on two coercible types, such as Age and Int? But in fact Haskell programmers often use newtypes precisely so that they can give a different type-class instance (for comparison, say) for Age than for the underlying Int. Type functions are no different;”

On se sert des types synomymes pour introduire des NOMS. ces noms ne doivent pas etre identifies pour les CLIENTS de ces noms. Les type functions, type classes sont clients, il faut leur cacher l’equation en notre possession (Age = Int).

yet more trouble

> data TF a = MkTF (F a)
> to :: Bool TF Int
> to b = MkTF b
> 
> from :: TF Age Char
> from (MkTF c) = c

this will fail

> vf2 = from . cvt . to

cvt utilise une preuve qui doit rester privee. a l’exterieur, les differences de noms doivent creer des differences

“This problem is important .. because the same issues will arise in any type system that combines type-level dispatch and coercion lifting.”

Coercion lifting : if for two types φ and ψ we have φ ∼ ψ (for example, if they are the abstract and concrete types of a newtype declaration), then T φ ∼ T ψ for any type constructor T .

qui n’est valable que d’un point de vue INTERNE ou les noms n’ont pas d’importance

FC2

• On peut voir Age et Int comme deux noms differents => “we can view Age and IntCode as two different codes that both map to the type Int”

• “the important distinction between codes and types is that they have different definitions of equality. In the encoding above, the codes Age and IntCode are different codes, but their interpretations are equal types” differentes definition de l’egalite, surtout preuves privees VS preuves publique. JE peux decider de creer deux noms que moi seul peut identifier. TU es force de penser qu’ils sont distincts. ce qui se passe avec les types abstraits et les valeurs, se passe aussi pour les fonctions de types et le systeme logique.

• “Age and Int are distinct when viewed at role code but equal when viewed at role type. Code equality is used to reason about the meaning of type-indexed functions and is finer-grained than type equality, which is used to determine which type coercions are safe”

“role type” : role dieu de la phase compilation, qui ne voit que l’utilisation finale : c’est un Int ou c’est un Bool ? Les autres subtilites sont detruites. Je peux devenir un dieu local et forcer mes clients a faire une distinction que moi seul peut lever, mais je reste soumis a mon dieu (qui identifie les types).

on a une hierarchie de dieu, et une relation d’ordre.

Description de FC2

FC2 is ex- pressive enough to capture indexed type functions, newtype and newtype deriving,GADTs,existentialandnesteddatatypes, and much more.

First, FC2 provides polymorphic datatypes,

Second, FC2 includes first-class proofs of type equality that witness safe coercions introduced during compilation

Syntax directed typechecking

Programs in FC2 can abstract over coercions reflecting a particular type equal- ity (written Λc : φ1 ∼ φ2.e), pass a coercion as an argument to such a function (written e γ), and use a coercion to cast a term from one type to another (written e ◃ γ). These explicit coercions, written γ, make typechecking FC2 programs syntax-directed.

The syntax of an FC2 term encodes its typing derivation

Why is this important?

• The idea is that the compiler’s front end performs perhaps-complex type inference on the source program, and records the proofs generated by inference directly in the syntax of the FC2 intermediate language.

• The optimiser transforms FC2 terms, perhaps radically.

At any point one can check the consistency of the resulting FC2 program using a simple, fast, syntax- directed typechecker; this consistency check has proven to be an extremely powerful aid to getting the compiler right. It is just as easy to find the type of an arbitrary FC2 term, an ability that is used extensively inside GHC.

Ma syntaxe reflete parfaitement la construction des proprietes logiques dont je veux parler, et toute l’information pour retrouver/verifier un propriete est dans mon terme, avec toutes les etapes intermediaires

FC2 types and kinds

Types in FC2 are classified by pairs κ of the form η/R, where :

• the kind η ensures (as usual) that types are well-formed structurally

• the role R that determines the precision at which they can be analyzed.

Codes (which distinguish Age and Int) have role C, whereas types (which identify them) have role T.

Par exemple :

The distinction between codes and types allows us to give infor- mative kinds to type constructors:

• The Maybe type (Section 2.1) has kind ⋆/T → ⋆, indicating that Maybe treats its argument parametrically (les proprietes logiques de Maybe s’expriment via le dieu compilation, et s’imposent a tous)

• The types K, F, and TF (Section 2.2) all use type indexing and therefore have kind ⋆/C → ⋆. (les proprietes de logiques de )

These kinds in turn support the key insight of this paper: it is only safe to lift coercions through functions with parametric kinds

So Maybe Age ∼ Maybe Int holds but TF Age ̸∼ TF Int.

Parce que Maybe se refere au dieu compilation qui s’impose aux autres dieux locaux, qui ne sont que des intercesseurs. Tandis que les TF sont des clients de Dieux non precises, potentiellement autres que celui de la compilation