Haskell GADTs - faire un type de Tensor typées pour la géométrie de Riemann

Question

Je veux faire un type mise en œuvre sûre du calcul Tensor dans Haskell en utilisant GADT de, de sorte que les règles sont les suivantes:

1. tenseurs sont metrices n-dimentionelles avec indecies qui peut être «à l'étage» ou «en bas» par exemple: - est un Tenseur sans indecies (un scalaire), est un Tenseur avec un index 'en haut', est un tenseur avec un tas de 'en haut' et ' downside 'indecies

2. Vous pouvez ajouter un tenseur du même type, ce qui signifie qu'ils ont la même signature d'inde. l'indice 0e du premier tenseur est du même type (haut ou en bas) que l'indice 0e du second tenseur et ainsi de suite ...

   ~~~~ OK

   ~~~~ pAS OK

3. Vous pouvez MULTIPLIER tenseurs et obtenir de plus gros tenseurs, avec les concaténer ees,:

Je veux que le type vérificateur de Haskell ne me permettrait pas d'écrire du code qui n » t suivez ces règles, il ne compilerait pas autrement.

Voici ma tentative à l'aide GADTs:

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE ExistentialQuantification #-} 
{-# LANGUAGE TypeOperators #-} 

data Direction = T | X | Y | Z 
data Index = Zero | Up Index | Down Index deriving (Eq, Show) 

plus :: Index -> Index -> Index 
plus Zero x = x 
plus (Up x) y = Up (plus x y) 
plus (Down x) y = Down (plus x y) 

data Tensor a = (a ~ Zero) => Scalar Double | 
       forall b. (a ~ Up b) => Cov (Direction -> Tensor b) | 
       forall b. (a ~ Down b) => Con (Direction -> Tensor b) 

add :: Tensor a -> Tensor a -> Tensor a 
add (Scalar x) (Scalar y) = (Scalar (x + y)) 
add (Cov f) (Cov g) = (Cov (\d -> add (f d) (g d))) 
add (Con f) (Con g) = (Con (\d -> add (f d) (g d))) 

mul :: Tensor a -> Tensor b -> Tensor (plus a b) 
mul (Scalar x) (Scalar y) = (Scalar (x*y)) 
mul (Scalar x) (Cov f) = (Cov (\d -> mul (Scalar x) (f d))) 
mul (Scalar x) (Con f) = (Con (\d -> mul (Scalar x) (f d))) 
mul (Cov f) y = (Cov (\d -> mul (f d) y)) 
mul (Con f) y = (Con (\d -> mul (f d) y)) 

Mais je suis en train:

Couldn't match type 'Down with `plus ('Down b1)'                                                  
    Expected type: Tensor (plus a b)                                                      
     Actual type: Tensor ('Down b)                                                      
    Relevant bindings include                                                       
     f :: Direction -> Tensor b1 (bound at main.hs:28:10)                                                
     mul :: Tensor a -> Tensor b -> Tensor (plus a b)                                                 
     (bound at main.hs:24:1)                                                       
    In the expression: (Con (\ d -> mul (f d) y))                                                  
    In an equation for `mul':                                                       
     mul (Con f) y = (Con (\ d -> mul (f d) y)) 

Quel est le problème?

Answer 1

plus est juste une fonction des valeurs de type Index

>>> plus Zero Zero 
Zero 
>>> plus Zero (Up Zero) 
Up Zero 

donc il ne peut pas apparaître dans une signature de type, comme les choses sont. Vous voulez utiliser le type "promu" où Zero, Up Zero etc. sont des types. Ensuite, vous pouvez écrire une fonction de type et tout compile.

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE ExistentialQuantification #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE TypeFamilies #-} 

data Direction = T | X | Y | Z 
data Index = Zero | Up Index | Down Index deriving (Eq, Show) 

-- type function Plus 
type family Plus (i :: Index) (j :: Index) :: Index where 
    Plus Zero x = x 
    Plus (Up x) y = Up (Plus x y) 
    Plus (Down x) y = Down (Plus x y) 

-- value fuction plus 
plus :: Index -> Index -> Index 
plus Zero x = x 
plus (Up x) y = Up (plus x y) 
plus (Down x) y = Down (plus x y) 

data Tensor (a :: Index) where 
    Scalar :: Double -> Tensor Zero 
    Cov :: (Direction -> Tensor b) -> Tensor (Up b) 
    Con :: (Direction -> Tensor b) -> Tensor (Down b) 

add :: Tensor a -> Tensor a -> Tensor a 
add (Scalar x) (Scalar y) = (Scalar (x + y)) 
add (Cov f) (Cov g) = (Cov (\d -> add (f d) (g d))) 
add (Con f) (Con g) = (Con (\d -> add (f d) (g d))) 

mul :: Tensor a -> Tensor b -> Tensor (Plus a b) 
mul (Scalar x) (Scalar y) = (Scalar (x*y)) 
mul (Scalar x) (Cov f) = (Cov (\d -> mul (Scalar x) (f d))) 
mul (Scalar x) (Con f) = (Con (\d -> mul (Scalar x) (f d))) 
mul (Cov f) y = (Cov (\d -> mul (f d) y)) 
mul (Con f) y = (Con (\d -> mul (f d) y)) 

Il n'y avait aucune ambiguïté dans Plus mais je aurais pu utiliser la désambiguïsation tique ' pour signaler que je traitais avec le niveau de type Zero, Up etc.

type family Plus (i :: Index) (j :: Index) :: Index where 
    Plus 'Zero x = x 
    Plus ('Up x) y = 'Up (Plus x y) 
    Plus ('Down x) y = 'Down (Plus x y) 

TypeOperators vous permettrait d'écrire a + b plutôt que Plus a b ci-dessus.

type family (i :: Index) + (j :: Index) :: Index where 
    Zero + x = x 
    Up x + y = Up (x + y) 
    Down x + y = Down (x + y)