Haskell LLVM 绑定不明确类型

Question

我正在尝试开始使用 Haskell 的 LLVM 绑定。 Hello World 是一个很好的起点。

以下内容来自绑定作者的博客。

bldGreet :: CodeGenModule (Function (IO ()))
bldGreet = do
    puts <- newNamedFunction ExternalLinkage "puts" :: TFunction (Ptr Word8 -> IO Word32)
    greetz <- createStringNul "Hello, World!"
    func <- createFunction ExternalLinkage $ do
      tmp <- getElementPtr greetz (0::Word32, (0::Word32, ()))
      call puts tmp -- Throw away return value.
      ret ()
    return func

它无法编译。
相反，我得到“模棱两可的类型变量n0' in the constraint: (type-level-0.2.4:Data.TypeLevel.Num.Sets.NatI n0) arising from a use ofgetElementPtr0' 可能的修复：添加修复这些类型变量的类型签名“

这是一个有效的变体

llvmModule :: TFunction (IO Word32)
llvmModule = 
    withStringNul "Hello world!" $ \s -> do 
    puts <- newNamedFunction ExternalLinkage "puts" :: TFunction (Ptr Word8 -> IO Word32)
    main <- newNamedFunction ExternalLinkage "main" :: TFunction (IO Word32)
    defineFunction main $ do
      tmp <- getElementPtr0 s (0::Word32, ())
      _ <- call puts tmp
      ret (0::Word32)
    return main

第一个似乎更自然。我的问题是第一个歧义是什么，我该如何解决。我的第二个问题是为什么第二个不模棱两可。

Answer 1

好的。所以我解决了这个问题。这确实是一个类型类的东西。它只会让我更加困惑。但是，我确实有解决方案的答案。但请随时帮助我理解。首先，一些挖掘。函数 createStringNul 有类型

createString :: String -> TGlobal (Array n Word8)

很好。编译器遇到的问题是 Array 类型中的“n”不明确。它实际上可以是世界上的任何东西。查找，数组，你看到了

newtype Array n a

现在不是那么明显了，但是经过一点挖掘，特别是在调用 getElementPtr 时，我们发现 n，实际上应该是一个 Nat n，这是一种类型级别的方法来固定大批。现在，Array n a 的定义实际上并不关心它实际上只是 [a] 的类型同义词。所以你可以使用 D0 或 D9 或任何你想要的 Data.TypeLevel.Num.Reps 包裹。固定数组的大小，而这个函数实际上并没有考虑到一个好主意。但无论如何，改变 greetz

这是有趣的部分...我没想到它会起作用。 D0 应该是 0，所以我不明白为什么它允许我在一个 0 大小的“数组”中存储这么多字符 但是，如果你查看源代码，就会立即清楚实际上并不是类型限制重视。

好吧，无论如何，在编译时意识到 createStringNul 已被弃用，而 withStringNul 是首选。除了我不完全理解 withStringNul 的类型是如何工作的。

Answer 2

createStringNul is marked as deprecated 在当前版本的llvm (3.0.1.0) 中。使用withStringNul：

import Data.Word
import LLVM.Core

bldGreet :: CodeGenModule (Function (IO ()))
bldGreet = do
    puts <- newNamedFunction ExternalLinkage "puts" :: TFunction (Ptr Word8 -> IO Word32)
    func <- withStringNul "Hello, World!" $ \greetz ->
      createFunction ExternalLinkage $ do
        tmp <- getElementPtr greetz (0::Word32, (0::Word32, ()))
        _ <- call puts tmp -- Throw away return value.
        ret ()
    return func

至于第一个示例中导致错误的原因，这与withStringNul 具有更多信息类型这一事实有关：withStringNul :: String -> (forall n . Nat n => Global (Array n Word8) -> a) -> a -- cf.到createStringNul :: String -> TGlobal (Array n Word8)。 withStringNul 的函数参数有一个higher-rank type - 这意味着该函数适用于所有n，其中n 是一个自然数。

如果你真的想使用createStringNul，你可以通过为greetz添加显式类型签名来编译第一个示例：

{-# LANGUAGE TypeOperators #-}
module Test
       where

import Data.Word
import Data.TypeLevel.Num.Reps
import LLVM.Core

bldGreet :: CodeGenModule (Function (IO ()))
bldGreet = do
    puts <- newNamedFunction ExternalLinkage "puts" :: TFunction (Ptr Word8 -> IO Word32)
    greetz <- createStringNul "Hello, World!"
    func <- createFunction ExternalLinkage $ do
      tmp <- getElementPtr (greetz :: Global (Array (D1 :* D3) Word8)) (0::Word32, (0::Word32, ()))
      call puts tmp -- Throw away return value.
      ret ()
    return func

:* 类型构造函数comes from the type-level package 用于构造类型级别的数字。 D1 :* D3 表示数组大小为 13。