List of any `DataKind` in GADT

Question

Renouncement

GADT and DataKinds are unexplored territory for me, so some of the limitations and possibilities are unknown to me.

Question

So, I am writing AST for an emitter of JavaScript code, and I have identified one edge case between expressions, and that is whether they can be a link or not. Therefore, I used GADTS and datakinds to introduce this aspect of the semantics of JavaScript expressions. Ast looks something like this.

A 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 great and dandy because the assignment expression requires that the first expression be a reference as a property expression ( "test".shadyProperty ) or reference / identifier.

Problem

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

 [a, 1, true, ab] 

In my AST, however, this is not legal because there are several 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 happens instead ??? for type? A similar problem occurs when I want to build a constructor for JSObject and JSFunctionCall, since they are also expressions.

Idris soul

In Idris ??? will look something like this.

 data JSExp : Bool -> Type where JSArray : List (JSExp _) -> JSExp False JSNumber : Float -> JSExp False JSBool : Bool -> JSExp False -- ... 

Potential souls

Type of packaging

One soul that is not like Idris will have a wrapper type like this

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

This will make my library's api rude, and that is not what I'm looking for.

In summary

I am looking for the equivalent found in Idris and an explanation of the consequences of the decision. If there is no equivalent, then the solution to the next best is what I'm looking for.

Answer 1

You can use existences:

 {-# LANGUAGE GADTs, DataKinds, PolyKinds #-} data Exists :: (k -> *) -> * where This :: px -> 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 sugar:

 infixr 5 !: (!:) :: px -> [Exists p] -> [Exists p] x !: xs = This x : xs test = let aref = JSReference "a" in JSArray $ aref !: JSNumber 2 !: JSBool True !: JSProperty aref "b" !: []