GADT中任何`DataKind`的列表

Question

放弃

GADTs和DataKinds对我来说是未开发的领域,因此我不了解它们的一些限制和功能.

问题

所以我正在为JavaScript代码发射器编写一个AST,并且我已经确定了表达式之间的一个边缘情况,那就是它们可以是引用或不引用.所以我使用GADTS和datakinds来键入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

  -- ...

潜在的灵魂

包装类型

一个不像伊德里斯那样的灵魂,会有这样的包装类型

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

这会使我的图书馆的api变得粗糙,而不是我正在寻找的.

综上所述

我正在寻找在Idris中找到的等效物,并解释了该解决方案的含义.如果没有相应的东西,那么下一个最好的东西的解决方案就是我正在寻找的东西.

Answer 1

你可以使用存在:

{-# 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" !: []