haskell - 将类型的类型约束移除为满足约束的值。 IE。 Num a => a 到 Int

Question

我正在使用一个名为 CLaSH 的系统。对于那些不熟悉它的人来说，它的设计方式允许您使用 Haskell 开发 FPGA。

我正在尝试创建一个无符号值。

定义于:https://hackage.haskell.org/package/clash-prelude-0.10.11/docs/src/CLaSH-Sized-Internal-Unsigned.html#Unsigned

类似于:

2 :: Unsigned 3

有效。我希望能够做类似的事情:

x = 3

2::Unsigned x

但是我得到了错误:

(KnownNat x1) 没有由文字“2”产生的实例

Possible fix:

 add (KnownNat x1) to the context of

 an expression type signature: Unsigned x1

 In the expression: 2 :: Unsigned x

 In an equation for `it': it = 2 :: Unsigned x

然后我尝试在同一个文件中定义“fromInteger#”。

let y=fromInteger# x

返回类型

y :: KnownNat n => Unsigned n

有了那个“y”，我可以通过添加一个指定大小的无符号来给它一个大小。

y + (2 :: Unsigned 3)

这给出了 5

it :: Unsigned 3

我怎样才能得到类似的东西

2::Unsigned x

如果我做不到，为什么我做不到？

编辑:使用模板 Haskell 可以完成我需要的操作。请参阅下面的代码并链接到 CLaSH 组解释

https://groups.google.com/forum/#!topic/clash-language/uPjt8i0lF0M .

我想要的可以在编译时完成。运行时是不可能的。

Answer 1

如果我没理解错的话，您希望能够在类型签名中将变量引用为类型级自然数。为此，您必须将 x 声明为类型(type 或 data)而不是值。正是值和类型之间的这种区别将 Haskell 与旧的依赖类型语言区分开来，在这些语言中，您可以自由地引用类型中的声明，而不必担心值和类型之间的差异。所以，试着让你的代码看起来像这样:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module Lib where

import Data.Proxy
import GHC.TypeLits

data Unsigned (a :: Nat)
type X = 2

main :: IO ()
main =
  print (Proxy :: Proxy (Unsigned X))

不过，恐怕我对 Clash 一无所知，所以我可能不了解全貌。