Evaluating Parameterized Types

[crockeea]

Consider a type

newtype Zq q = Zq Int

where arithmetic is mod q. I'd like to be able to share a value of this type using something similar to share in NanoFeldspar from syntactic-2.0, and then evaluate that expression. My understanding is that this requires the use of BindingT, which requires the constraint Typeable t (Internal a) for the instance Syntactic (a -> b).

Our q values will be reified, so I can't make instances for (e.g.)

data Five
data Zq5Type  a where Zq5Type  :: Zq5Type  (Full (Zq Five))

and even if I could, I don't wouldn't want to since there are an infinite number of moduli that could be used. Everything I've tried fails when I try to make a TypeEq instance (required for evalSem). Is there an easy way to evaluate a syntax tree which shares a value with a reified type parameter?

[emilaxelsson]

I might have misunderstood the problem, but how about this solution?
https://gist.github.com/emilaxelsson/ed5ffd25f11e56e6ccfc

It has a single Typeable instance for all q values. To add new q values, just add an empty type (e.g. Q100), extend the SQ type, add an instance for the Sing class and extend the sqEq function.

(The code could be simplified a bit using the DataKinds extension and the singletons library, but the underlying idea is the same.)

[emilaxelsson]

This gave me a reason to finally try out type level naturals. The code got a lot simpler, and it works for any natural number q!!

Hope this helps.

[crockeea]

Thanks, that's a helpful example. However we aren't using TypeLits. Instead, we're reifying moduli using Data.Reflection:

reify (3::Int) (\(_::Proxy q) ->
   let x = 5 :: Zq q
   in ....

It appears from your TypeLits example and from the NanoFeldspar example that we need some way of testing for equality of the reified types. I guess I'm asking if there's a way to evaluate and share without this equality test, since there isn't an obvious way (to me) to test equality of reified types.

In particular, I was thought that instead of using a list of pairs to represent the environment (which requires embedding the types into the Dynamic type), a type list could be used to obviate the need for dynamic typing at all, which should also removed the need for type equality tests.

[crockeea]

I dug into TypeLits to see how it implements equality: it just reflects the value and uses unsafeCoerce if the values are equal! I expected something a little fancier/safer/elegant. Reflection/unsafeCoerce can easily be used with reflection as well, so your code is extremely helpful, thank you!

[emilaxelsson]

Glad it worked out for you!

FYI:
Your comment about evaluation without dynamic typing made me curious to try this out in Syntactic. The result is here:
https://gist.github.com/emilaxelsson/2a94e5df4a5ee4bd7b16

The representation is a bit complicated. If one really wanted to pursue this track, it might be better to change the AST type to keep track of environments.

The price for this way of handling bound variables is that the interface is more complicated. For example, the type of share is now:

share :: Exp e a -> ((forall e' . Suff e' (a,e) => Exp e' a) -> Exp (a,e) b) -> Exp e b

Note that there is currently no way of printing these expressions, since variables are represented as functions, but this should be fixable.

Anyway, this was a fun exercise!

[crockeea]

Emil, we've spent the last week working with your solution, but we keep running into problems. For example, it doesn't allow us to use -XPolyKinds: http://stackoverflow.com/questions/23764545/using-type-equality-with-polykinds

We would really encourage you to look into the type-list solution further (or some other direction than BindingT), and feel it is too burdensome to have to make a BlahType for each type Blah you want to be able to bind. With this solution, we are looking at adding at least 4 such types, times the number of Kinds we would like to use, if we use the answer to the StackOverflow post.

This issue is causing us such a headache that we are considering attempting to use or modify your type-lists code. Since my next step in development is probably trying to better-understand your type-list code, I would be happy to see if I can make it any cleaner and report back here.

[emilaxelsson]

Before going on with the more strongly typed solution -- would it work to use the standard Typeable class (which is kind-polymorphic nowadays) instead?

If so, it should be possible to change BindingT to

data BindingT a
  where
    VarT :: Typeable a => Name -> BindingT (Full a)
    LamT :: Typeable a => Name -> BindingT (b :-> Full (a -> b))

[crockeea]

We think that would suffice, if it means we could put any Data.Typeable type in the environment (and evaluate it).

I just want to verify that this would remove the need for the Syntactic.Typeable class. I'm currently in a situation where I have to explicitly give a Typeable ExprTypes a constraint. This means that someone later would be unable add a Syntactic.Typeable type to the ExprTypes list and evaluate it! The example is here: https://gist.github.com/crockeea/86de62101a4e31b2ece1

There is one caveat to your solution: we would ideally like to use reflected types from Data.Reflection, which do not currently have a Data.Typeable instance. However, are willing to work around that for now. It's just something to keep in mind when you choose Typeable over strongly typed environments: not all types are Typeable. Specifically, you can see my datatype here and the Reflection issue.

[emilaxelsson]

I've changed to using Typeable in BindingT (747ac89). But I see from the discussion in reflection that it might not solve the problem :-(

[crockeea]

On the plus side, your code is now much cleaner (except for the deprecated TypeUniverse files still hanging around). However, we are running into more troublese with this. It turns out that (fast) reified types aren't the only things that aren't Typeable.

GHC doesn't export Typeable instances for any promoted types, though there's a ticket to fix this. However, comment 3 indicates that a fix to that ticket won't fix Nats, which was going to be our substitute for reflection. In a private communication with Iavor, it appears Typeable Nats are coming, but I shouldn't hold my breath.

Is the type list solution a possibility?

[emilaxelsson]

Is the type list solution a possibility?

Absolutely! (But we should make it a separate module beside the other ones.)

What did you think about the solution given here?

If it works for you, I think I can fix so that the terms can also be printed/analyzed. I have to think about how this approach plays with the Syntactic class. Ideally, you'd want share to be overloaded as in NanoFeldspar.

[crockeea]

I think that solution will work. It's not ideal, but it would be nice to have something until some point in the distance future when most (all?) types are Typeable.

[emilaxelsson]

I've now incorporated the well-scoped terms into Syntactic; see the "Well-scoped terms" section in Functional.hs.

I've also provided an example file which I hope will help you get going.

I think this is the best we can do. There are many ways to encode well-typed and well-scoped terms[1], but as far as I can tell, they all result in ugly types (like that of share). The only way around this is to use dynamic type casting (i.e. Typeable) AFAICT.

[1]: The encoding I chose was with efficient evaluation in mind.