Closed crockeea closed 10 years ago
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.)
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.
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.
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!
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!
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.
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))
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.
I've changed to using Typeable
in BindingT
(747ac89). But I see from the discussion in reflection that it might not solve the problem :-(
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 Nat
s, 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?
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.
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.
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.
Consider a type
where arithmetic is mod
q
. I'd like to be able to share a value of this type using something similar toshare
in NanoFeldspar from syntactic-2.0, and then evaluate that expression. My understanding is that this requires the use ofBindingT
, which requires the constraintTypeable t (Internal a)
for the instanceSyntactic (a -> b)
.Our
q
values will be reified, so I can't make instances for (e.g.)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 forevalSem
). Is there an easy way to evaluate a syntax tree which shares a value with a reified type parameter?