haskell - 从 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]) )并给我一个 GF (Polynomial Int) ([2, 0, 1]) 类型的伽罗瓦域.
我知道 [2, 0, 1]不是有效类型，但我看到 Data.Singletons可以创建类似的类型

(SCons STrue (SCons SFalse SNil))

为 [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 文字和 [...]是类型 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。