Question: Should DAG.Expression remain untyped?

[frp-arduino]

Question: Should DAG.Expression remain untyped?

[rickardlindberg]

The DSL.Expression is a phantom type for DAG.Expression:

newtype Expression a = Expression { unExpression :: DAG.Expression }

The phantom type guaranties type correct DAGs. The only point where I'm a bit uncertain if this works is in the Num instance.

[rickardlindberg]

Removed discussion of solution from title.

[mvcisback]

@rickardlindberg , yes I'm aware it's a phantom type. I'm unsure how it asserts the correctness of DAG`'s. For example, nothing is stopping me from defining

foo :: DSL.Expression Bool
foo = DAG.Expression $ ListConstant []

[rickardlindberg]

If you only use the functions in the DSL module, you can only create correct DAGs.

In the example you showed, you can indeed create invalid DAGs, but then you need to use functions from the DAG module.

So the phantom type ensures that users of the DSL create correct DAGs. But it does not ensure that creators of the DSL (us) create correct DAGs.

Maybe GADTs will also solve that problem. In that case, I think it's a better option.

This article seems to prefer phantom types over GATSs: http://augustss.blogspot.se/2007/06/representing-dsl-expressions-in-haskell.html

[mvcisback]

@rickardlindberg yes, I think its slightly unreasonable to assume that the user (including us) will never need to write extensions to the DSL. The GADT ensure that this is possible.

Another concern of mine is whether the code generator uses the types consistently. I suspect it does given that it works, but this acts as a test to make sure they remain consistent.

[mvcisback]

Just read the article. The big concern seems to be that GADTs isn't standard.
This is a bit of a judgment call. I don't mind being tied to ghc, given its general pervasiveness.

The other sticking point is that the evaluator now needs a typed environment. I don't think this is an issue since we are targeting C which is typed.

[rickardlindberg]

Just read this and found it quite helpful:

https://en.wikibooks.org/wiki/Haskell/GADT

[mvcisback]

@rickardlindberg exactly, we just replace eval with a compiler in CodeGen. GADTs would allow us to enforce type safety all the way down.

[rickardlindberg]

From Lennart's article:

GADTs is really the way to go, but it has the disadvantage of not being standard Haskell. It can also get somewhat cumbersome when we have variables; the evaluator now needs a typed environment.

I don't understand the second part about cumbersome with variables.

[mvcisback]

@rickardlindberg I think he's referring to having a variable constructor in your DSL:

data Expr a where
    IntConst :: Int -> Expr Int
    Variable :: Expr a -> Expr a

or alternatively (depending on how it needs to be encoded)

data Ref a = Ref a

data Expr a where
    IntConst :: Int -> Expr Int
    Variable :: Expr a -> Expr (Ref a)

He the talks about

the evaluator now needs a typed environment.

Which was exactly the point of the GADTs! (as in the wiki link). I think its a pretty bad argument.

The whole ghc exclusive part sure, but not because I'm worried about a typed evaluation....that's what I want unless I'm emulating an untyped language (like python)

[rickardlindberg]

In the DAG, we have Input Int which is a variable of arbitrary type. Will that be hard to express using GADT?

I don't undertstand your example:

Variable :: Expr a -> Expr a

Don't you need a name of some kind? Or the index in Input Int?

Probably I should study GADTs more.

[mvcisback]

Sure, it'd probably make sense to use an identifier for the variable

i.e.

Variable :: Identifier -> Expression a -> Expression a

As a GADT, Input Int Because Input :: Int -> Expression Int
That main point is that one can specify the output type.

[rickardlindberg]

But in the case of Input, we don't know the type beforehand. An input can be of any type.

Anyway, late night here now, so I should probably get some sleep now and think more about this tomorrow :-)

[mvcisback]

haha, ok.

Also, I seem to have misunderstood what input was. Yes in the case of any type you would just define

Input :: Int -> Expression a

Then the first use of it will set the type.

I.E.

myInput :: Expression Int
myInput = Input 0

which is the exact same situation as the phantom type.