类型安全的稳定指针

Question

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

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

Answer 1

StablePtr a 的 C 对应物是 void * 的 typedef -- 在 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 中，可以使用 type-generic expressions 减少这种混乱， 这可以在没有组合爆炸的情况下添加“正确”类型的演员表。 尽管如此，没有人利用它编写 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、volatile ......

例如，指向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这个类型是明目张胆的谎言！！ T 类型的值实际上是 void * 指向 StablePtr T 类型的一些 Haskell 端表示，并且肯定不是指向 C 函数的指针！尽管如此，传递T 将保持类型安全。

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

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

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

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

---

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