从 Haskell 中的列表构造依赖类型

Question

我想用 Haskell 为 Galois 字段编写一个库。伽罗瓦域由其不可约多项式定义。只有具有相同的伽罗瓦域的伽罗瓦域元素才能相加。我想将多项式提升为我的伽罗瓦域的类型，例如，具有多项式 [1, 2, 3] 的伽罗瓦域与具有多项式 [2, 0, 1] 的伽罗瓦域具有不同的类型。这样我可以确保只能添加​​具有相同伽罗瓦域的伽罗瓦域元素。这可能吗？

我的多项式数据类型如下所示：

newtype Polynomial a = Polynomial [a]

我的 Galois 字段数据类型如下所示：

data GF irr a = GF {
    irreducible :: irr
  , q :: PrimePower
}

所以我想要一个构造函数，它接受一个多项式（例如(Polynomial [2, 0, 1])）并给我一个类型的 Galois 域GF (Polynomial Int) ([2, 0, 1])。我知道这[2, 0, 1]不是一个有效的类型，但我看到使用Data.Singletons可以创建类似的类型

(SCons STrue (SCons SFalse SNil))

for [True, False]，但我不知道如何从我的列表中构造喜欢这些类型的类型[2, 0, 1]以及构造函数的外观。

Answer 1

由于卢克已经评论，[2, 0, 1] 是实际上是一个有效的类型。

Prelude> :set -XDataKinds -XPolyKinds 
Prelude> data A x = A deriving Show
Prelude> A :: A [2,0,1]
A

其中数字文字实际上是类型级Nat文字，并且[...]是类型种类的列表值构造函数的提升版本。这可以通过用“prime-quote 语法”来明确表达

Prelude> A :: A '[2, 0, 1]
A

……所以，这个任务其实很简单。你可以使用

{-# LANGUAGE DataKinds, KindSignatures #-}

import GHC.TypeLits (Nat)

newtype Polynomial a = Polynomial [a]

data GF (irr :: Polynomial Nat) = GF {q :: PrimePower}

正如 Luke 所说，尽管类型级计算不如在完全依赖类型的语言中工作得那么好。如果你真的想用这个做证明，你应该考虑切换到 Idris、Agda 或 Coq。