Using type families to define runtime representation and evaluation strategy?
I'm interested in the feasibility of extending the compiler using a construct similar to type synonym families to determine runtime representation and evaluation strategy for types. Can anybody point me to existing work in this area? I'm not sure of the exact terminology to be using here so my description is going to be fuzzy and probably off the mark on a few points. If anybody could help me clarify what I'm trying to described that would be appreciated. What I imagine is an open construct that be evaluated at compile time to determine: - How the data for a type is represented in memory. Whether values are boxed or unboxed etc. - How an expression should be represented. As a lazy evaluation thunk (weak head normal form?) or evaluated to normal form. - How a expression should be reduced. Since "the best" evaluation strategy depends on the application the equations should be open. For one application a data structure should be evaluated the normal form but not another. This is why the construct should be open much like type synonym families. One application could define an instance that declares the value should be reduced to HNF when defined while the other application could define an instance that declares the value to be reduced to WHNF. Still, the library implementor needs the ability to define reasonable defaults. If the construct was closed I don't think these requirements could be satisfied. This resembles extending the Control.Parallel.Strategies evaluation strategies and adaptive-container's container representation to be represented by type level equations. Control.Parallel.Strategies has a good interface but littering the equations with expressions declaring the evaluation strategy seems awkward. Preferably the evaluation strategy should be definable in parallel to the equations when possible. Strictness annotations already resemble the start of such a construct. And any such construct would have to be able to take the place of strictness annotations. Cheers, Corey O'Connor
coreyoconnor:
I'm interested in the feasibility of extending the compiler using a construct similar to type synonym families to determine runtime representation and evaluation strategy for types. Can anybody point me to existing work in this area?
There's a lot of work on controlling data representations with associated types -- indeed, that was their original use case! Also related might be the new paper "Types are calling conventions" -- Don
On Wed, Jun 3, 2009 at 1:09 PM, Don Stewart
coreyoconnor:
I'm interested in the feasibility of extending the compiler using a construct similar to type synonym families to determine runtime representation and evaluation strategy for types. Can anybody point me to existing work in this area?
There's a lot of work on controlling data representations with associated types -- indeed, that was their original use case!
What I'm imagining as a use case would be taking the canonical example from the adaptive-containers: l :: [(Int, Int)] l = [ (x,y) | x <- [1..3], y <- [x..3] ] A module that uses "l" that requires the same data representation as the List(Pair Int Int) type when using adaptive containers would then include an equation somewhat like the following: type instance DataRep [(Int, Int)] = List(Pair Int Int) However all list code would then need to be augmented to take into consideration the DataRep associated type. Correct? Seems like this augmentation could be done implicitly by the compiler. Potentially going off the deep end: Data representation is how a block of memory represents a type such that the representation supports the required evaluation semantic. The data representation for a data constructor where the definition equation is evaluated lazily is different than the data representation for the same constructor where the definition is evaluated strictly. One requires representing the state of the thunk in memory while the other does not. Assuming that is accurate then equations could be represented implicitly parametrized over the data representation equations for each type. Kinda akin to how equations using type class equations are implicitly parametrized by the dictionary representing the witness of that type class for a given type. Except I'm imagining something at the type level instead of value level. Regardless. I need to read up on associated types and try some experiments before I can make claims on what they can and what they cannot do. :-)
Also related might be the new paper "Types are calling conventions"
From the abstract it does sound related. Thanks! I'll add it to my reading pile.
Cheers, Corey O'Connor
On 3 Jun 2009, at 20:49, Corey O'Connor wrote:
I'm interested in the feasibility of extending the compiler using a construct similar to type synonym families to determine runtime representation and evaluation strategy for types. Can anybody point me to existing work in this area?
You may also want to look at work by Paul Levy on "Call-by-push-value" and more recently, Noam Zeilberger (and others at CMU) on focussing. Both use types to control when and how evaluation happens. Hope this helps, Wouter This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
participants (3)
-
Corey O'Connor -
Don Stewart -
Wouter Swierstra