1

免责声明

GADTs 和 DataKinds 对我来说是未开发的领域，所以我不知道它们的一些限制和功能。

问题

因此，我正在为 JavaScript 代码发射器编写 AST，并且我已经确定了表达式之间的一个边缘情况，即它们可以是引用也可以不是引用。因此，我使用 GADTS 和数据类型来键入 JavaScript 表达式语义的这一方面。ast 看起来像这样。

表达式 AST 的子集

-- at the moment I'm just using a bool to identify if the expression 
-- behaves as an reference, but I'll probably change it due to the fact
-- a bool is pretty vague

data JSExp :: Bool -> * where

  JSNumber :: Double -> JSExp False
  JSBool :: Bool -> JSExp False

  JSReference :: Text -> JSExp True
  JSProperty :: JSExp a -> Text -> JSExp True
  JSAssign :: JSExp True -> JSExp b -> JSExp b

这看起来很好，很花哨，因为赋值表达式要求第一个表达式是引用，如属性表达式 ( "test".shadyProperty) 或引用/标识符。

问题

现在我想添加一个数组文字表达式，在 JavaScript 中，这个列表中的内容并不重要，所以像这样的列表是合法的

[a, 1, true, a.b]

然而，在我的 AST 中，这是不合法的，因为列表中有多种类型

data JSExp :: Bool -> * where

  -- ...

  JSArray :: [JSExp ???] -> JSExp False

let aref = JSReference "a"
in  JSArray [aref, JSNumber 2, JSBool True, JSProp aref "b"]

什么可以代替???类型？当我想为 JSObject 和 JSFunctionCall 构建一个构造函数时，也会出现类似的问题，因为它们也是表达式。

伊德里斯的灵魂

在伊德里斯???看起来像这样。

data JSExp : Bool -> Type where

  JSArray : List (JSExp _) -> JSExp False
  JSNumber : Float -> JSExp False
  JSBool : Bool -> JSExp False

  -- ...

潜在的灵魂

包装类型

一种与 Idris 不同的灵魂，会拥有这样的包装器类型

data JSExpWrap = Refs (JSExp True) | NoRef (JSExp False)

这会使我图书馆的 api 变得粗糙，这不是我想要的。

总之

我正在寻找在 Idris 中找到的等价物，以及对解决方案含义的解释。如果没有等价物，那么下一个最好的解决方案就是我正在寻找的。

4

1 回答 1

6

您可以使用存在主义：

{-# LANGUAGE GADTs, DataKinds, PolyKinds #-}

data Exists :: (k -> *) -> * where
  This :: p x -> Exists p

data JSExp :: Bool -> * where
  ...
  JSArray :: [Exists JSExp] -> JSExp False

test = let aref = JSReference "a"
       in  JSArray [This aref, This (JSNumber 2), This (JSBool True), This (JSProperty aref "b")]

或者加点糖：

infixr 5 !:
(!:) :: p x -> [Exists p] -> [Exists p]
x !: xs = This x : xs

test = let aref = JSReference "a"
       in  JSArray $ aref !: JSNumber 2 !: JSBool True !: JSProperty aref "b" !: []
于 2015-02-07T23:54:39.343 回答