haskell - 将类型上的类型约束移除为满足约束的值。即 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”产生的实例

 

可能的修复：

 将 (KnownNat x1) 添加到

 表达式类型签名：无符号 x1

 在表达式中： 2 :: Unsigned x

 在 `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 一无所知，所以也许我没有全貌。