哈斯克爾GADTs - 做一個類型安全的張量類型黎曼幾何

我想在Haskell中使用GADT的類型安全的實現張量計算的，所以規則是：哈斯克爾GADTs - 做一個類型安全的張量類型黎曼幾何

張量正維metrices與可以是'樓上'或'樓下'的indecies，例如： - 是一個沒有indecies（一個標量）的張量，是一個帶有'樓上'索引的張量，是一張張'樓上'和'樓下'indecies
您可以添加相同類型的張量，這意味着它們具有相同的indecies簽名。第一張量的第0指數是相同的類型（樓上或樓下）作爲第二張量的第0索引等的...

~~~~~~行

~~~~ NOT OK
即可成倍張量和獲得更大張量，與indecies級聯：

所以我想這哈斯克爾的類型檢查器不會讓我寫那並不是碼Ť遵循這些規則，否則不會編譯。

這裏使用我嘗試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))

，但我發現：

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))

問題是什麼？

來源

2017-04-01 user47376

你寫了'plus'作爲（值級別）函數，但你試圖在一個類型中使用它。 Haskell無法做到這一點。（它認爲'mul'的返回類型中的'plus'是一個類型參數。）使用類型族。 –

我用type-operators – user47376

我可以推薦你考慮[對張量無座標的方法]（http://hackage.haskell.org/package/linearmap-category-0.3.2.0/docs/Math-LinearMap-Category .html），沒有那些愚蠢的索引... – leftaroundabout

plus只是在類型Index

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

，因此它不能出現在類型簽名的值的函數，如事情。您想要使用「提升」類型，其中Zero，Up Zero等是類型。然後你可以編寫一個類型函數並編譯所有的東西。

{-# 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))

有沒有歧義Plus但我可以利用多義性蜱'信號，我正在處理的類型級別Zero，Up等

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將允許你寫a + b而不是Plus a b以上。

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

來源

2017-04-01 13:21:59 Michael

哈斯克爾GADTs - 做一個類型安全的張量類型黎曼幾何

回答

相關問題