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

Question

我想在 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])）并给我一个GF (Polynomial Int) ([2, 0, 1]) 类型的Galois 字段。 我知道[2, 0, 1] 不是有效类型，但我看到Data.Singletons 可以创建类似

(SCons STrue (SCons SFalse SNil))

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

Answer 1

正如 Luke 已经评论的那样，[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”来明确表达

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。

Answer 2

似乎“提升”值将仅用作标记。对于我们只希望它作为标签工作的情况，但很难使用DataKinds 将所需的值提升到类型级别，一种可能的替代方法是在值上附加一个“幽灵”类型标签，通过一个多态的咒语。考虑这个帮助模块：

{-# LANGUAGE RankNTypes #-}
module Named (Named,forgetName,name) where

newtype Named n a = Named a -- don't export the constructor

forgetName :: Named n a -> a
forgetName (Named a) = a

name :: a -> ( forall name. Named name a -> r ) -> r
name x f = f ( Named x ) -- inside the callback, "x" has a "name" type tag attached

还有其他依赖它的模块：

module GF (Polynomial(..),GF,stuff,makeGF,addGF) where

import Named

newtype Polynomial a = Polynomial [a]

data GF a = GF { -- dont' export the constructor
    _stuff :: Int -- don't export the bare field
}

stuff :: GF a -> Int
stuff (GF x) = x

makeGF :: Named ghost (Polynomial Int) -> Int -> GF ghost
makeGF _ = GF 

addGF :: Named ghost (Polynomial Int) -> GF ghost -> GF ghost -> GF ghost
addGF _ x1 x2 = GF (stuff x1 + stuff x2)

我不可能让这个模块的 clients 将两个具有不同幽灵标签的 GF 值相加。他们创建幽灵标签的唯一方法是通过name，并且他们没有重新标记Named 值或GF 值的方法——我们小心地隐藏了构造函数和裸字段以防止这种情况发生。所以这将编译：

module Main where

import Named
import GF

main :: IO ()
main = print $
    name (Polynomial [2::Int,3,4]) $ \ghost ->
      let x1 = makeGF ghost 3
          x2 = makeGF ghost 4
       in stuff (addGF ghost x1 x2)

但这不会：

main :: IO ()
main = print $
    name (Polynomial [2::Int,3,4]) $ \ghost1 ->
        name (Polynomial [3::Int]) $ \ghost2 ->
          let x1 = makeGF ghost1 3
              x2 = makeGF ghost2 4
           in stuff (addGF ghost1 x1 x2)