4

我花了很多时间在我的数据类型中编码不变量，现在我正在努力通过 FFI 将我的库暴露给 C。我没有跨语言障碍编组数据结构，而是简单地使用不透明的指针来允许 C 构建一个 AST，然后在evalHaskell 上只需要将一个字符串编组到 C。

这是一些更有启发性的代码。

-- excerpt from Query.hs
data Sz = Selection | Reduction deriving Show

-- Column Datatype

data Column (a :: Sz) where
    Column  :: String -> Column Selection
    BinExpr :: BinOp  -> Column a -> Column b -> Column (OpSz a b)
    AggExpr :: AggOp  -> Column Selection -> Column Reduction

type family OpSz (a :: Sz) (b :: Sz) where
    OpSz Selection Selection = Selection
    OpSz Selection Reduction = Selection
    OpSz Reduction Selection = Selection
    OpSz Reduction Reduction = Reduction

data Query (a :: Sz) where
    ... etc


-- excerpt from Export.hs

foreign export ccall "selection"
    select :: StablePtr [Column a] -> StablePtr (Query b) -> IO (StablePtr (Query Selection))

foreign export ccall 
    add :: StablePtr (Column a) -> StablePtr (Column b) -> IO (StablePtr (Column (OpSz a b)))

foreign export ccall 
    mul :: StablePtr (Column a) -> StablePtr (Column b) -> IO (StablePtr (Column (OpSz a b)))

foreign export ccall
    eval :: StablePtr (Query Selection) -> IO CString

然而，据我所知，这似乎将类型安全抛到了窗外。基本上任何 C 交给 Haskell 的东西都会被认为是那种类型，这完全否定了我在 Haskell 中编写 dsl 的原因。有什么方法可以让我获得使用 StablePtr 的好处并保持类型安全？我想要的最后一件事是在 C 中重新实现不变量。

4

1 回答 1

1

C 的对应物StablePtr a是 typedef，用于void *在 FFI 边界失去类型安全性。

问题在于 有无限多的可能性a :: *，因此对于StablePtr a。除非使用非常单一的 C 类型（见下文），否则无法在具有有限类型系统（没有参数类型！）的 C 中对这些类型进行编码。

在您的特定情况下，a, b :: Sz我们只有有限的案例，一些 FFI 工具可以帮助对这些案例进行编码。尽管如此，这仍会导致案例的组合爆炸：

typedef struct HsStablePtr_Selection_ { void *p; } HsStablePtr_Selection;
typedef struct HsStablePtr_Reduction_ { void *p; } HsStablePtr_Reduction;

HsStablePtr_Selection
add_Selection_Selection(HsStablePtr_Selection a, HsStablePtr_Selection b);
HsStablePtr_Selection
add_Selection_Reduction(HsStablePtr_Selection a, HsStablePtr_Reduction b);
HsStablePtr_Selection
add_Reduction_Selection(HsStablePtr_Reduction a, HsStablePtr_Selection b);
HsStablePtr_Reduction
add_Reduction_Reduction(HsStablePtr_Reduction a, HsStablePtr_Reduction b);

在 C11 中，可以使用泛型表达式来减少这种混乱，这可以添加“正确的”类型转换而不会发生组合爆炸。尽管如此，没有人利用它编写 FFI 工具。例如：

void *add_void(void *x, void *y);
#define add(x,y) \
   _Generic((x) , \
   HsStablePtr_Selection: _Generic((y) , \
      HsStablePtr_Selection: (HsStablePtr_Selection) add_void(x,y), \
      HsStablePtr_Reduction: (HsStablePtr_Selection) add_void(x,y)  \
      ) \
   HsStablePtr_Reduction: _Generic((y) , \
      HsStablePtr_Selection: (HsStablePtr_Selection) add_void(x,y), \
      HsStablePtr_Reduction: (HsStablePtr_Reduction) add_void(x,y)  \
      ) \
   )

（上面的转换是从指向结构的指针，所以它们不起作用，我们应该使用结构文字，但我们忽略它。）

在 C++ 中，我们可以利用更丰富的类型，但 FFI 旨在使用 C 作为通用语言来绑定到其他语言。

理论上，可以利用 c 具有的唯一类型构造函数来实现 Haskell（单态！）参数类型的可能编码：指针、数组、函数指针、const、易失性......

例如，指向的稳定指针type T = Either Char (Int, Bool)可以表示如下：

typedef struct HsBool_ { void *p } HsBool;
typedef struct HsInt_ { void *p } HsInt;
typedef struct HsChar_ { void *p } HsChar;
typedef struct HsEither_ HsEither;  // incomplete type
typedef struct HsPair_ HsPair;      // incomplete type

typedef void (**T)(HsEither x1, HsChar x2
                  void (**)(HsPair x3, HsInt x4, HsBool x5));

当然，从C的角度来看，类型T是明目张胆的谎言！！type 的值T实际上会void *指向一些 Haskell 端的类型表示，StablePtr T而不是指向 C 函数的指针！尽管如此，传递T将保持类型安全。

请注意，上述只能在非常弱的意义上称为“编码”，即从单态Haskell类型到C类型的单射映射，完全无视C类型的语义。这样做只是为了确保，如果将此类稳定指针传递回 Haskell，C 端会进行一些类型检查。

我使用了 C 的不完整类型，因此永远无法在 C 中调用这些函数。我使用了指向指针的指针，因为 (IIRC) 指向函数的指针无法void *安全地转换为。

请注意，这种复杂的编码可以在 C 中使用，但可能难以与其他语言集成。例如，可以使用 JNI + FFI 使 Java 和 Haskell 进行交互，但我不确定 JNI 部分能否处理如此复杂的编码。也许，void *更实用，尽管不安全。

安全编码多态函数、GADT、类型类......留待未来工作：-P

TL;DR：FFI 可以更努力地将静态类型编码为 C，但这很棘手，目前对此没有很大的需求。也许在未来这可能会改变。

于 2016-04-08T17:44:59.827 回答