GADT中的任何`DataKind`列表 [英] List of any `DataKind` in GADT

问题描述

免责声明

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

问题

因此，我正在为JavaScript代码发射器编写一个AST，并且我已经确定了表达式之间的一个边界情况，那就是它们可以是参考或不参与。所以我使用GADTS和datakinds来输入JavaScript表达语义的这个方面。 AST看起来像这样。

表达式的子集AST

   - 此刻我只是使用bool来确定表达式
是否作为引用，但我可能会因此改变它
  - 一个bool很漂亮模糊的
 
 data JSExp :: Bool  - > *其中
 
 JSNumber :: Double  - > JSExp False 
 JSBool :: Bool  - > JSExp False 
 
 JSReference :: Text  - > JSExp True 
 JSProperty :: JSExp a  - >文字 - > JSExp True 
 JSAssign :: JSExp True  - > JSExp b  - > JSExp b 
  

由于赋值表达式要求第一个表达式是一个引用像一个属性表达式（test.shadyProperty ）或一个引用/标识符。

问题

现在我想添加一个数组字面值表达式，在JavaScript中它不应该在这个列表中包含什么，所以像这样的列表是合法的

  [a，1，true，ab] 
  

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

  data JSExp :: Bool  - > *其中
 
  -  ... 
 
 JSArray :: [JSExp ???]  - > JSExp False 
 
 let aref = JSReferencea
 in JSArray [aref，JSNumber 2，JSBool True，JSProp arefb] 
  

这个类型的地方 ??? 是什么？当我想为JSObject和JSFunctionCall构建一个构造函数时，会出现类似的问题，因为这些也是表达式。

$ b

Idris的灵魂

在Idris ??? 看起来像这样。

  data JSExp：Bool  - >键入其中
 
 JSArray：List（JSExp _） - > JSExp False 
 JSNumber：Float  - > JSExp False 
 JSBool：Bool  - > JSExp False 
 
  -  ... 
  

Potenial soultions

包装类型

一种不像Idris的灵魂人物，会有这样的包装类型

  data JSExpWrap = Refs（JSExp True）| NoRef（JSExp False）
  

这会让我的图书馆的api变得糟糕，而且这不是我的寻找。

总结

我正在寻找在伊德里斯发现的等价物，解决方案的含义。如果没有相应的解决方案，下一个最好的解决方案就是我正在寻找的解决方案。 解决方案

您可以使用existentials：

  { - ＃LANGUAGE GADTs，DataKinds，PolyKinds＃ - } 
 
 data Exists ::（k - > *） - > *其中
 This :: p x  - >存在p 
 
 data JSExp :: Bool  - > *其中
 ... 
 JSArray :: [Exists JSExp]  - > JSExp False 
 
 test = let aref = JSReferencea
 in JSArray [This aref，This（JSNumber 2），This（JSBool True），This（JSProperty arefb）] 
  

或者加上一些糖：

  infixr 5！：
（！:) :: px  - > [Exists p]  - > [Exists p] 
x！：xs = This x：xs 
 
 test = let aref = JSReferencea
 JSArray $ aref！：JSNumber 2！：JSBool True！ ：JSProperty arefb！：[] 
  

Disclaimer

GADTs & DataKinds are unexplored territory for me, so some of the limitations and capabilities of them are unknown to me.

The Question

So I'm writing an AST for a JavaScript code emitter, and I've identified one edge case between expressions and that is that they can either be a reference or not. So I've used GADTS and datakinds to type this aspect of JavaScript expression semantics. The ast looks something like this.

Subset of the expression 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

This looks all fine and dandy, because an assignment expression requires the first expression to be a reference like a property expression ("test".shadyProperty) or a reference/identifier.

The problem

Now I want to add an array literal expression, in JavaScript it shouldn't matter what is in this list so lists like this are legal

[a, 1, true, a.b]

In my AST however this is not legal because there are multiple types in the list

data JSExp :: Bool -> * where

  -- ...

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

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

What goes in the place of ??? for the type? A similar problem occurs when I want to build out a constructor for JSObject's and JSFunctionCall's, as these are also expressions.

Idris's soultion

In Idris ??? would look something like this.

data JSExp : Bool -> Type where

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

  -- ...

Potenial soultions

Wrapping type

One soultion that isn't like the Idris one, would to have a wrapper type like this

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

This would make the api of my library gross and it's not what I'm looking for.

In Summary

I'm looking for the equivalent that's found in Idris, and an explanation of the implications of the solution. If there's no equivalent, a solution of the next best thing is what I'm looking for.

解决方案

You can use existentials:

{-# 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")]

Or with some sugar:

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

这篇关于GADT中的任何`DataKind`列表的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！