Using trick from IRC (Thank bartavelle) plus a `formal` proof of injectivity for `MixVar`, this works. No need for Singleton / Bool.

Expr GADTs.lhs

On commence par quelques kilos d'extensions :

> {-# LANGUAGE GADTs, KindSignatures, DataKinds, TypeFamilies, TypeOperators,
>              ScopedTypeVariables, FlexibleInstances, ConstraintKinds, PolyKinds,
>              StandaloneDeriving, NoMonomorphismRestriction #-}
> {-# OPTIONS -Wall #-}

> module Expr where

Et deux trois imports :

> import Data.Type.Equality
> import Unsafe.Coerce (unsafeCoerce)
> import Data.Type.Bool

Je veux faire un petit DSL de calcul qui me permet de representer des opérations avec :

- Des litéraux (`Integer`)
- Des litéraux (`Bool`)
- Des opérations binaires entre deux sous expression qui renvoient une expression.

L'idée de base c'est de représenter cela avec un ADT comme ceci :

> data Expr = IntE Int -- Un literal int
>           | BoolE Bool -- In literal bool
>           | AddE Expr Expr -- Une opération Binaire d'addition
>           | EqualE Expr Expr -- Une opération Binaire d'égalité
>           | VarE -- Une variable
>           deriving (Show) -- Pour l'affichage

On peut donc representer de nombreuses expressions :

> exprs :: [Expr]
> exprs = [
>          AddE (IntE 1) (IntE 2),   -- 1 + 2
>          AddE (IntE 1) VarE,        -- 1 + x
>          EqualE (IntE 1) (IntE 2), -- 1 == 2
>          EqualE VarE (BoolE True)   -- x == True
>         ]

On peut aussi écrire deux fonctions d'évaluation :

- `evalVar` qui sait évaluer une expression connaissant la valeur d'une variable.
- `eval` qui évalue mais sans connaitre la variable.

-- Bon, c'est quoi le type de `eval`, cela prend une `Expr` et cela renvoie quoi ?
-- Et bien déjà là je suis perdu, j'aimerais renvoyer un `Int` ou un `Bool` en fonction du type de l'expression interne,
-- Mais je ne sais pas faire. Bon, je vais renvoyer un `Result` :

> data Result = ResultBool Bool | ResultInt Int -- Soit un `Int` soit un `Bool`
>           deriving (Show) -- Pour l'affichage

Pareil, c'est quoi le type de la variable ? On ne sait pas trop, alors on passe un `Result` :

> evalVar :: Result -> Expr -> Result
> evalVar _ (IntE i) = ResultInt i
> evalVar _ (BoolE b) = ResultBool b
> evalVar v (AddE a b) = case (evalVar v a, evalVar v b) of
>                       (ResultInt a', ResultInt b') -> ResultInt (a' + b')
>                       _ -> error "Cannot add bool expression"
> evalVar v (EqualE a b) = case (evalVar v a, evalVar v b) of
>                        (ResultInt a', ResultInt b') -> ResultBool (a' == b')
>                        (ResultBool a', ResultBool b') -> ResultBool (a' == b')
>                        _ -> error "Cannot compare expression of different type"
> evalVar v VarE = v

On peut définir `eval` à partir de `evalVar` :

> eval :: Expr -> Result
> eval e = evalVar (error "Cannot eval Var because it is not known") e

Ici `error` c'est une exception runtime. On utilise `evalVar` en lui
passant la valeur, qui est une exception. Mais elle ne sera lancée que
en cas d'utilisation. C'est un example interessant d'évaluation
paresseuse en Haskell.

Examples :

> -- >>> eval (AddE (IntE 1) (IntE 2))
> -- ResultInt 3
> -- >>> eval (EqE (IntE 1) (IntE 1))
> -- ResultBool True
> -- >>> evalVar (ResultInt 5) (AddE (IntE 2) Var)
> -- ResultInt 7

Ces codes souffrent de pas mal de défauts :

- Il faut encapsuler la variable d'entrée et deencapsuler la valeur de sortie
- On peut crée des Expressions qui n'ont pas de sens, résultant en des erreur lors de l'évaluation :

> -- >>> eval (AddE (BoolE True) (IntE 5)) -- Addition d'un Bool et d'un Int
> -- >>> eval (EqE (BoolE True) (IntE 5)) -- Comparaison d'un Bool et d'un Int

- On peut passer des variables qui n'ont pas le bon type ou évaluer
  des expressions qui ont une variable sans en fournir une :

> -- >>> evalVar (ResultInt 5) (AddE Var (IntE 5)) -- La variable n'a pas le bon type
> -- >>> eval (AddE Var (IntE 5)) -- On essaye d'évaluer une expression qui a une variable sans fournir sa valeur

Tout ces points sont énervants, peut-on les fixer ?

Pour cela nous allons commencer par utiliser un GADTs. C'est un ADT
mais un peu plus typé. Reecrivons tout d'abord le type `Expr` avec la
syntaxe `GADTs` :

> data ExprGADT where
>      IntEG :: Int -> ExprGADT -- Un literal int
>      BoolEG :: Bool -> ExprGADT -- In literal bool
>      AddEG :: ExprGADT -> ExprGADT -> ExprGADT -- Une opération Binaire d'addition
>      EqualEG :: ExprGADT -> ExprGADT -> ExprGADT -- Une opération Binaire d'égalité
>      VarEG :: ExprGADT -- Une variable
>           deriving (Show) -- Pour l'affichage

La syntaxe est un peu différente, chaque cas est listé sur un ligne
comme un prototype de fonction. On vois par example que la fonction
(ou constructeur) `AddEG` prend deux `ExprGADT` et renvoie un
`ExprGADT`.

Nous allons maintenant ajouter un type paramètre a notre `ExprGADT`,
pour en faire `ExprGADTT t` :

> data ExprGADTT t where
>      IntEGT :: Int -> ExprGADTT Int -- Un literal int
>      BoolEGT :: Bool -> ExprGADTT Bool -- In literal bool
>      AddEGT :: ExprGADTT Int -> ExprGADTT Int -> ExprGADTT Int -- Une opération Binaire d'addition
>      EqualEGT :: Eq t => ExprGADTT t -> ExprGADTT t -> ExprGADTT Bool -- Une opération Binaire d'égalité
>      VarEGT :: ExprGADTT t -- Une variable

> deriving instance Show (ExprGADTT t) -- pour l'affichage

Peut de choses change, mais on vois maintenant que le constructeur
`IntEGT` renvoie une expression `ExprGADTT` parametrisé par un
`Int`. Le literal `Bool` renvoie bien une expression
`Bool`. L'addition ne marche qu'entre `Int` et renvoie un `Int` et
l'égalité marche entre deux type `t` identiques, comparable (le `Eq t
=>`) et renvoie un `Bool`.

On peut maintenant écrire de nouveau `eval` :

> evalT :: ExprGADTT t -> t
> evalT (IntEGT i) = i
> evalT (BoolEGT b) = b
> evalT (AddEGT a b) = evalT a + evalT b
> evalT (EqualEGT a b) = evalT a == evalT b
> evalT VarEGT = error "variable"

Le code de `evalT` est BEAUCOUP plus simple, et n'inclue pas tous les
cas d'exception qui ne sont plus possibles. En effet, on ne peut plus
crée d'expression qui n'ont plus de sens tel que l'addition entre une
sous expression `Int` et une sous expression `Bool`. Il n'y a plus non
plus besoin de packing et dépacking :

> -- >>> evalT (AddEGT (IntEGT 1) (IntEGT 2))
> -- 3
> -- >>> evalT (EqEGT (IntEGT 1) (IntEGT 1))
> -- True

Une expression du type `AddEGT (IntEGT 1) (BoolEGT True)` ne compile plus !

Nous n'avons pas réglé le problème de la variable qui peut toujours
être présente, et à l'heure actuelle nous ne sommes pas capable
d'écrire `evalVarT` puisque il faudrait pouvoir connaitre le type de
la variable, ce qui n'est pas le cas. On peut aussi construire des
expression encore un peu tordue contenant deux variables de type
different, comme `EqualEGT (EqualEGT Var (IntEGT 5)) Var`, qui est
équivalent à (x == 5) == x), où x est à la fois un int et un bool.

Attention, c'est là que cela pique un peu plus.

On vas ajouter deux types parametriques à notre Expression, que nous
rebatisons `Expr' exprt varStatus vart` pour la forme.

Ici :

  - exprt est le type de l'expression (Int ou Bool) comme utilisé avant
  - varStatus est un Booléan au niveau du type qui represente la présence ou nom de variable dans l'expression
  - vart est le type de la variable, si présente

> -- thank you bartavelle
> data Expr' exprt varStatus vart where
>   IntE' :: Int -> Expr' Int 'False vart -- Unliteral Int ne contient pas de variable. Et le type de la variable est indéfini.
>   BoolE' :: Bool -> Expr' Bool 'False vart -- Un literal Bool ne contient pas de variable et le type de la variable est indéfini
>   -- Là c'est plus complexe, pour AddE' et EqE'. L'expression contient une variable si l'un des deux sous expression contient une variable (d'ou le OU)
>   -- et le type de la variable doit être le même dans les sous expressions et il devient le type de la variable de l'expression
>   AddE' :: Expr' Int varStatus vart -> Expr' Int varStatus' vart -> Expr' Int (varStatus || varStatus') vart
>   EqE' :: Eq t => Expr' t varStatus vart -> Expr' t varStatus' vart -> Expr' Bool (varStatus || varStatus') vart
>   Var' :: Expr' vart 'True vart
>
> deriving instance Show (Expr' a b c)

Quelques examples d'expressions, cela marche toujours comme il faut.

> -- Some expresion examples
> v = IntE' 5
> v' = Var'
> v'' = EqE' (BoolE' True) Var'
> v''' = AddE' (IntE' 5) (Var')
> v'''' = EqE' Var' Var'
> v''''' = (EqE' (EqE' (AddE' (IntE' 1) (IntE' 2)) (IntE' 3)) (BoolE' True))

Evaluer avec une Variable est plutôt simple, on ne met aucune contrainte sur le type de la variable ou sa présence.

> evalVar' :: a -> Expr' t t' a -> t
> evalVar' _ (IntE' i) = i
> evalVar' _ (BoolE' b) = b
> evalVar' v (AddE' a b) = evalVar' v a + evalVar' v b
> evalVar' v (EqE' a b) = evalVar' v a == evalVar' v b
> evalVar' v Var' = v

Evaluer sans variable est plus complexe, car on fixe le fait qu'une expression n'a pas de variable.
Ce n'est pas un problème pour les 2 premiers cas de literals :

> eval' :: Expr' t 'False t' -> t
> eval' (IntE' i) = i
> eval' (BoolE' b) = b

Mais cela devient problématique pour les opérations binaires. En
effet, connaissant le fait qu'une expression ne contient pas de
variable (i.e. son second type paramétrique est 'False), comment
savoir que les deux sous expression sont ausi expressions sans
variable.

Il se trouve que nous nous savons que c'est le cas, puisque on utilise le || binaire :

False || False -> False *
False || True -> True
True || False -> True
True || True -> True

On observe que le seul cas ou a || b est False c'est si a est False et
b est False. On peut dire que || est injective sur un sous domaine.

Cependant le compilateur ne le sait pas. Il faut donc lui fournir une
preuve de cette information.

Et là on rentre dans le chamanisme, j'ai gratté pendant quelques temps
avant d'obtenir ça et j'ai du mal à l'expliquer.

> eval' (AddE' a b) = add a b
>   where
>     add :: forall a b t'. ((a || b) ~ 'False) => Expr' Int a t' -> Expr' Int b t' -> Int
>     add exprA exprB = case proof :: (a :~: 'False, b :~: 'False) of
>       (Refl, Refl) -> eval' exprA + eval' exprB
> eval' (EqE' a b) = eq a b
>   where
>     eq :: forall a b t t'. (Eq t, (a || b) ~ 'False) => Expr' t a t' -> Expr' t b t' -> Bool
>     eq exprA exprB = case proof :: (a :~: 'False, b :~: 'False) of
>       (Refl, Refl) -> eval' exprA == eval' exprB


Voici la preuve, qui pour l'instant est trichée (Je dis juste que c'est bon) :

> -- unsafe proof of (Partial) injectivity for (||)
> -- THIS IS WRONG AND UNSAFE, but I don't know how to write it otherwise
> proof
>     :: ((a || b) ~ 'False)
>     => (a :~: 'False, b :~: 'False)
> proof = unsafeCoerce (Refl, Refl)

ça compile, mais c'est pas top :)

data CanHaveVar t = NopeVar | CanVar t | ReallyVar t


type family PVarBin a where
  PVarBin 'NopeVar = 'NopeVar
  PVarBin ('CanVar t) = 'CanVar t 
  PVarBin ('ReallyVar t) = 'CanVar t 

data Expr' t t' where
  IntE' :: Int -> Expr' Int 'NopeVar
  BoolE' :: Bool -> Expr' Bool 'NopeVar
  AddE' :: Expr' Int (PVarBin x) -> Expr' Int (PVarBin x) -> Expr' Int x
  EqE' :: Eq t => Expr' t (PVarBin x) -> Expr' t (PVarBin x) -> Expr' Bool x
  Var' :: Expr' t ('ReallyVar t)

eval' :: Expr' t 'NopeVar -> t
eval' (IntE' i) = i 
eval' (BoolE' b) = b 
eval' (AddE' a b) = eval' a + eval' b 
eval' (EqE' a b) = eval' a == eval' b