我想用 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])
)并给我一个 GF (Polynomial Int) ([2, 0, 1])
类型的伽罗瓦域.我知道
[2, 0, 1]
不是有效类型,但我看到 Data.Singletons可以创建类似的类型(SCons STrue (SCons SFalse SNil))
为
[True, False]
,但我不知道如何从我的列表中构建类似这些类型 [2, 0, 1]
以及构造函数的样子。
最佳答案
正如卢克已经评论过的,[2, 0, 1]
实际上是一个有效的类型。
Prelude> :set -XDataKinds -XPolyKinds
Prelude> data A x = A deriving Show
Prelude> A :: A [2,0,1]
A
其中数字文字实际上是类型级别
Nat
文字和 [...]
是类型 kind 的列表值构造函数的提升版本。这可以通过用“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。
关于haskell - 从 Haskell 中的列表构造依赖类型,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59673078/