Haskell GADTs - 为黎曼几何制作类型安全的张量类型答案

【问题标题】：Haskell GADTs - making a type-safe Tensor types for Riemannian geometryHaskell GADTs - 为黎曼几何制作类型安全的张量类型
【发布时间】：2017-04-01 12:16:31
【问题描述】：

我想使用 GADT 在 Haskell 中实现张量演算的类型安全，所以规则是：

张量是具有“楼上”或“楼下”指标的 n 维度量，例如： - 是没有指标的张量（标量），是具有一个“楼上”索引的张量, 是一个带有一堆“楼上”和“楼下”不雅点的张量
您可以添加相同类型的张量，这意味着它们具有相同的 indecies 签名。第一个张量的第 0 个索引与第二个张量的第 0 个索引的类型相同（楼上或楼下），依此类推...

~~~~好的

~~~~不行
您可以乘以张量并获得更大的张量，并连接不定数：

所以我希望 Haskell 的类型检查器不允许我编写不遵循这些规则的代码，否则它不会编译。

这是我使用 GADT 的尝试：

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

有什么问题？

【问题讨论】：

您将plus 写为（值级别）函数，但您试图在类型中使用它。 Haskell 做不到。（它认为mul的返回类型中的plus是一个类型参数。）使用类型族。
我使用了类型运算符
我建议你也考虑a coordinate-free approach to tensors，没有那些愚蠢的索引......
@leftaroundabout 哇酷图书馆。不仅仅是一个抽象模型，还有一些主力——反演、特征值、...。谢谢指点！
我其实很喜欢索引符号。也许这只是一种偏见，我在这个符号中学习了广义相对论......

标签： haskell type-safety gadt data-kinds

【解决方案1】：

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)

【讨论】：