时间戳

首页 > 解决方案 > 从 Haskell 的列表中构造一个依赖类型

haskell - 从 Haskell 的列表中构造一个依赖类型

问题描述

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

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

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]以及构造函数的外观。

标签： haskellsingleton

解决方案

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

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

其中数字字面量实际上是类型级别的Nat字面量，并且[...]是类型类型的列表值构造函数的提升版本。这可以通过使用“prime-quote syntax”来明确表达</p> 

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。

推荐阅读