3

我正在使用一个名为 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  。 

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

4

1 回答 1

4

如果我理解正确,您希望能够在类型签名中将变量作为类型级别的自然值引用。为此,您必须声明x为类型(typedata)而不是值。正是这种值和类型之间的区别将 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 一无所知,所以也许我没有全貌。

于 2016-08-15T16:22:49.433 回答