
As I understand it, ATs were invented because FDs are "evil" and must never be used ever for any purpose. However, it doesn't seem to be possible to use ATs to do the same things that FDs can do. You can use ATs to write type functions, which take one type and return another type. This allows you to express type relationships in a very elegant way. However, what it does /not/ seem to allow you to do is express one-to-one relationships. For example, I'd like to be able to say that the next vector up from a Vector3 is a Vector4, and the next vector down is a Vector2. And I can say that. What I can't say is that the *only* next vector up is a Vector4. And thus, all my code is littered with ambiguous type warnings because although /currently/ there's only one class instance, somebody could come along some day and write another one. What am I missing?

Andrew Coppin
As I understand it, ATs were invented because FDs are "evil" and must never be used ever for any purpose. However, it doesn't seem to be possible to use ATs to do the same things that FDs can do.
You can use ATs to write type functions, which take one type and return another type. This allows you to express type relationships in a very elegant way. However, what it does /not/ seem to allow you to do is express one-to-one relationships.
For example, I'd like to be able to say that the next vector up from a Vector3 is a Vector4, and the next vector down is a Vector2. And I can say that. What I can't say is that the *only* next vector up is a Vector4. And thus, all my code is littered with ambiguous type warnings because although /currently/ there's only one class instance, somebody could come along some day and write another one.
I assume you mean something like this? ,---- | class NextOneUpFD this previous | this -> previous where ... | | instance NextOneUpFD Vector3 Vector4 where ... `---- If so, how does this not solve the issue? ,---- | class NextOneUpAT v where | type Next v | ... | | instance NextOneUpAT Vector3 where | type Next Vector3 = Vector4 | ... `---- -- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com IvanMiljenovic.wordpress.com

Ivan Lazar Miljenovic wrote:
I assume you mean something like this?
,---- | class NextOneUpFD this previous | this -> previous where ... | | instance NextOneUpFD Vector3 Vector4 where ... `----
More like class NextPrevFD next prev | next -> prev, prev -> next where... but yeah, that's the general idea.
If so, how does this not solve the issue?
,---- | class NextOneUpAT v where | type Next v | ... | | instance NextOneUpAT Vector3 where | type Next Vector3 = Vector4 | ... `----
Can I use that to go both up and down? Would the types be unambiguous? I guess I'll have to go try it out...

Andrew Coppin
Ivan Lazar Miljenovic wrote:
I assume you mean something like this?
,---- | class NextOneUpFD this previous | this -> previous where ... | | instance NextOneUpFD Vector3 Vector4 where ... `----
More like
class NextPrevFD next prev | next -> prev, prev -> next where...
but yeah, that's the general idea.
Oh, I wasn't sure you could do that.
If so, how does this not solve the issue?
,---- | class NextOneUpAT v where | type Next v | ... | | instance NextOneUpAT Vector3 where | type Next Vector3 = Vector4 | ... `----
Can I use that to go both up and down? Would the types be unambiguous? I guess I'll have to go try it out...
Depends on how you use it; it might need to have a "type Previous v" in there as well, but I'm not sure how well that will cope when you get to the "end of the line". One thing to note: GHC does not currently support superclass constraints, so it isn't possible to have something like: class (NextOneUpAT v1, NextOneUpAT v2, Next v1 ~ Next v2) => ... But you _can_ do so in a type signature for a function. -- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com IvanMiljenovic.wordpress.com

Andrew Coppin wrote:
Ivan Lazar Miljenovic wrote:
If so, how does this not solve the issue?
,---- | class NextOneUpAT v where | type Next v | ... | | instance NextOneUpAT Vector3 where | type Next Vector3 = Vector4 | ... `----
Can I use that to go both up and down? Would the types be unambiguous? I guess I'll have to go try it out...
Actually, this seems to work just fine as-is. (Famous last words...)

On 14 August 2010 11:19, Andrew Coppin
As I understand it, ATs were invented because FDs are "evil" and must never be used ever for any purpose. However, it doesn't seem to be possible to use ATs to do the same things that FDs can do.
You might want to read the "Language and Program Design for Functional Dependencies" paper by Mark P. Jones and Iavor Diatchki. In some situations fundeps are much cleaner than type funs, and cleanliness is virtuous surely?
participants (3)
-
Andrew Coppin
-
Ivan Lazar Miljenovic
-
Stephen Tetley