仿真“静态依赖类型”在Haskell中（如果需要，使用GHC扩展） [英] Emulate "static dependent types" in Haskell (if needed, with GHC extensions)

问题描述

假设我有一个类型类 Vec ，它实现了比方说有理数的向量空间的理论。

  class Vec a where 
（+）:: a  - > a  - > a 
 zero :: a 
  - 其余省略
  

数字n，我可以很容易地构造一个 Vec 的实例，其基础类型是有理列表的类型，并且实现了维度为n的向量空间。我们在以下方面取n = 3：

pre $ newtype RatList3 = RatList3 {list3 :: [Rational]}
instance VEC RatList3其中
V + W = RatList3（zipWith（前奏。+）（项目list3 v）的（项目list3瓦特））
零= RatList3（坐3（重复0））


对于另一个自然数，例如计算的数字，我可以写出

  f :: Int  - > Int 
fx = x * x  - 一些复杂的函数
n :: Int 
n = f 2 
 newtype RatListN = RatListN {listN :: [Rational]} 
 instance Vec RatListN其中
V + W = RatListN（zipWith（前奏。+）（listN v）（listN瓦特））
零= RatListN（取n（重复0））
  

现在我有两种类型，一种是维度为3的向量空间，另一种是维度为n的向量空间。但是，如果我想将模板中的实例声明放在实例Vec RatList？中，我不知道主程序最终会使用哪个模块，问题作为类型 RatList？不知道它属于哪个n。

为了解决这个问题，我试图做以下几行：

 类HasDim a其中
 dim :: Int 
 
实例（HasDim a，小数a）=> Vec [a]其中
v + w =​​ ... 
 zero = take dim（重复（fromRational 0））
 
  - 在主模块中
实例HasDim合理的地方
 dim = n  - 一些整数
  

这当然不起作用因为 HasDim 中的 dim 独立于类型变量 a 和实例（HasDim a）=> Vec [a] 目前还不清楚哪种类型的 dim 需要。我试图通过引入另一种类型来绕过第一个问题：

  newtype Dim a = Dim {idim :: Int} 
  

然后我可以写出

  class HasDim a其中
 dim :: Dim a 
  

然而，它是我不清楚如何在实例（HasDim a）=>中使用它。 Vec [a]其中。另外，我的整个解决方案对我来说看起来相当麻烦，而提出的问题看起来很简单。 （我认为使用C ++模板编写代码很容易。）

编辑

我已经除了ephemient的答案，因为没有类型算术，它以我想要的方式解决了我的问题。仅供参考，我的最终解决方案如下：

 类Vec a其中
 zero :: a 
  -  ... 
 
n :: Int 
n = 10 
 
 newtype RatListN = RatListN [Rational] 
 
实例Vec RatListN其中
 zero = RatListN。取n $ repeat 0 
  -  ... 
  

解决方案

这似乎是类型算术会让你得到一些你想要的东西的情况。 / b>

 数据零
数据Succ a 
类型One = Succ零
类型Two = Succ One 
 type Three = Succ Two 
  -  ... 
 
 class NumericType a where 
 toNum ::（Num b）=> a  - > b 
 instance NumericType Zero其中
 toNum = const 0 
实例（NumericType a）=> NumericType（Succ a）其中
 toNum（Succ a）= toNum a + 1 
 
 data RatList ab = RatList {list :: [b]} 
 instance（NumericType a，数字b）=> Vec（RatList a b）其中
 zero = RatList。 take（toNum（undefined :: a））$ repeat 0 
  

现在 RatList两个Int 和 RatList三个Int 是不同的类型。另一方面，这确实会阻止您在运行时实例化新维度。

Assume that I have a type class Vec that implements the theory of, say, vector spaces over the rationals.

class Vec a where
    (+)  :: a -> a -> a
    zero :: a
    -- rest omitted

Now given a natural number n, I can easily construct an instance of Vec whose underlying type is the type of lists of rationals and which implements a vector space of dimension n. We take n = 3 in the following:

newtype RatList3 = RatList3 { list3 :: [Rational] }
instance Vec RatList3 where
    v + w = RatList3 (zipWith (Prelude.+) (list3 v) (list3 w))
    zero  = RatList3 (take 3 (repeat 0))

For another natural number, for example a calculated one, I can write

f :: Int -> Int
f x = x * x -- some complicated function
n :: Int
n = f 2
newtype RatListN = RatListN { listN :: [Rational] }
instance Vec RatListN where
    v + w = RatListN (zipWith (Prelude.+) (listN v) (listN w))
    zero  = RatListN (take n (repeat 0))

Now I have two types, one for vector spaces of dimension 3 and one for vector spaces of dimension n. However, if I want to put my instance declaration of the form instance Vec RatList? in a module where I don't know which n my main program eventually uses, I have a problem as the type RatList? doesn't know which n it belongs to.

To solve the problem, I tried to do something along the following lines:

class HasDim a where
    dim      :: Int

instance (HasDim a, Fractional a) => Vec [a] where
    v + w = ...
    zero  = take dim (repeat (fromRational 0))

-- in the main module
instance HasDim Rational where
    dim = n -- some integer

This doesn't work, of course, because dim in HasDim is independent of the type variable a and in instance (HasDim a) => Vec [a] it is not clear which type's dim to take. I tried to circumvent the first problem by introducing another type:

newtype Dim a = Dim { idim :: Int }

Then I can write

class HasDim a where
    dim      :: Dim a

However, it is not clear to me how to use this in instance (HasDim a) => Vec [a] where. Also my whole "solution" looks rather cumbersome to me, while the posed problem looks simple. (I think it is easy to code this with C++ templates.)

EDIT

I have excepted ephemient's answer because without the type arithmetic it solved my problem the way I wanted to. Just for information, my final solution is along the following lines:

class Vec a where
    zero :: a
    -- ...

n :: Int
n = 10

newtype RatListN = RatListN [Rational]

instance Vec RatListN where
    zero = RatListN . take n $ repeat 0
    -- ...

解决方案

This seems like a case where type arithmetic would get you some of what you want.

data Zero
data Succ a
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
-- ...

class NumericType a where
    toNum :: (Num b) => a -> b
instance NumericType Zero where
    toNum = const 0
instance (NumericType a) => NumericType (Succ a) where
    toNum (Succ a) = toNum a + 1

data RatList a b = RatList { list :: [b] }
instance (NumericType a, Num b) => Vec (RatList a b) where
    zero = RatList . take (toNum (undefined :: a)) $ repeat 0

Now RatList Two Int and RatList Three Int are different types. On the other hand, this does prevent you from instantiating new dimensionalities at runtime…

这篇关于仿真“静态依赖类型”在Haskell中（如果需要，使用GHC扩展）的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！