haskell – Typesafe StablePtrs

2019年7月28日 178次阅读

我花了很多时间在我的数据类型中编码不变量,现在我正在通过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

据我所知,这似乎是把窗户安全抛出窗外.基本上无论C对Haskell的移交是否会被假定为完全否定我在Haskell中编写dsl的原因.有什么办法可以让我获得使用StablePtr并保持类型安全的好处吗？我想要的最后一件事是在C中重新实现不变量.

最佳答案 与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)  \
      ) \
   )

(上面的转换是从指向struct的指针,所以它们不起作用,我们应该使用struct literals,但让我们忽略它.)

在C中,我们可以使用更丰富的类型,但FFI意味着使用C作为绑定到其他语言的通用语言.

可以实现Haskell(单态！)参数类型的可能编码,理论上,利用唯一的类型构造函数c具有：指针,数组,函数指针,const,volatile,….

例如,类型为T = E(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中使用,但可能很难与其他语言集成.例如,Java和Haskell可以使用JNI FFI进行交互,但我不确定JNI部分是否可以处理这种复杂的编码.也许,void *更实用,尽管不安全.

安全地编码多态函数,GADT,类型类……留待将来的工作:-P

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

点赞