It seems like Haskell has two emerging idioms for parsing and fsms: GADTs and Arrows. I am thinking about using one of these idioms to represent server structure in a future version of HAppS but I'm not sure where to start. Why would one choose one or the other? -Alex- ______________________________________________________________ S. Alexander Jacobson tel:917-770-6565 http://alexjacobson.com
Hi
It seems like Haskell has two emerging idioms for parsing and fsms: GADTs and Arrows.
What about something else? If you limit yourself to the two things that look "new and cool" (where emerging is another word for new, and idiom seems to be the current Haskell word for cool), you miss out on all the tried and tested stuff.
I am thinking about using one of these idioms to represent server structure in a future version of HAppS but I'm not sure where to start. Why would one choose one or the other?
I would pick Arrows (over GADTs) because Arrows are Haskell, and are supported by multiple Haskell compilers. Other than that (as far as I was aware) these two things are massively different, so I wouldn't have thought it was a "one or the other" choice usually. Thanks Neil
I don't think I'm the only one confused here. Henrik Nilson in his paper on adding GADTs to Yampa comments that: However, the recent addition of Generalized Algebraic Data Types (GADTs) [26] to the list of Haskell extensions supported by the Glasgow Haskell Compiler (GHC) gives programmers a lot more freedom. GADTs are a limited form of dependent types, offering a considerably enlarged scope for capturing and thus en- forcing important code and data invariants statically. In particular, GADTs are just what is needed to address the problem discussed above since the key idea is to allow constructors that have more spe- cific types than usual, and to take that extra type information into account in individual case branches. GADTs would no doubt also offer an interesting alternative to the methods described by Baars and Swierstra [1] and Hughes [19]. [1] and [19] are papers about Arrows. I guess I'm also not sure what belongs in a GADT and what belongs in a typeclass e.g. here is an Arrow GADT data Arrow b c where Arr::(b->c) -> Arrow b c Compose::Arrow b c -> Arrow c d -> Arrow b d First::Arrow a b -> Arrow (a,c) (b,c) When Arrow is defined like this, rather than write instances you just various evaluation functions for the Arrow GADT. -Alex- ______________________________________________________________ S. Alexander Jacobson tel:917-770-6565 http://alexjacobson.com On Tue, 5 Dec 2006, Neil Mitchell wrote:
Hi
It seems like Haskell has two emerging idioms for parsing and fsms: GADTs and Arrows.
What about something else? If you limit yourself to the two things that look "new and cool" (where emerging is another word for new, and idiom seems to be the current Haskell word for cool), you miss out on all the tried and tested stuff.
I am thinking about using one of these idioms to represent server structure in a future version of HAppS but I'm not sure where to start. Why would one choose one or the other?
I would pick Arrows (over GADTs) because Arrows are Haskell, and are supported by multiple Haskell compilers. Other than that (as far as I was aware) these two things are massively different, so I wouldn't have thought it was a "one or the other" choice usually.
Thanks
Neil
On Thursday 07 December 2006 09:44, S. Alexander Jacobson wrote:
I guess I'm also not sure what belongs in a GADT and what belongs in a typeclass e.g. here is an Arrow GADT
data Arrow b c where Arr::(b->c) -> Arrow b c Compose::Arrow b c -> Arrow c d -> Arrow b d First::Arrow a b -> Arrow (a,c) (b,c)
When Arrow is defined like this, rather than write instances you just various evaluation functions for the Arrow GADT.
How would the GADT solution handle the behaviours captured in the other Arrow classes, eg ArrowIf, ArrowLoop etc? It doesn't seem right to just add constructors for all those extra functions. Daniel
Hi Alex, S. Alexander Jacobson wrote:
I guess I'm also not sure what belongs in a GADT and what belongs in a typeclass e.g. here is an Arrow GADT
data Arrow b c where Arr::(b->c) -> Arrow b c Compose::Arrow b c -> Arrow c d -> Arrow b d First::Arrow a b -> Arrow (a,c) (b,c)
When Arrow is defined like this, rather than write instances you just various evaluation functions for the Arrow GADT.
Indeed, there is a free choice (no pun) between this datatype and a class instance. The way I think about it, the datatype 'Arrow' above is the universal/free/(most general) instance of the class 'Arrow'. As you mention, specific instances of the class correspond to evaluation functions on this datatype. (In fact, this datatype presumably is the colimit of all instances of the 'Arrow' class, suitably interpreted as a functor.) In practice, you usually just want an instance; the universal datatype is only an extra layer of indirection. Sometimes however this datatype keeps useful extra information. I have used this approach once to allow algebraic manipulation of some kind of arrows: the GADT constructors make it possible to do pattern matching on the structure of the arrow. This is impossible if your arrow is some opaque function. Regards, Arie
Dear all, S. Alexander Jacobson wrote:
I don't think I'm the only one confused here. Henrik Nilson in his paper on adding GADTs to Yampa comments that: ... In particular, GADTs are just what is needed to address the problem discussed above since the key idea is to allow constructors that have more specific types than usual, and to take that extra type information into account in individual case branches. GADTs would no doubt also offer an interesting alternative to the methods described by Baars and Swierstra [1] and Hughes [19].
[1] and [19] are papers about Arrows.
I categorically deny being confused! :-) The comment refers to the methods Baars, Swierstra, and Hughes employ to encode type equality in order to be able to perform optimizations along similar lines as outlined in my paper. I was not at all proposing to use GADTs in place of arrows, and I cannot really see how the quote can be read as suggesting that. As Neil has already said: GADTs and arrows are just different kinds of entities. Best, /Henrik -- Henrik Nilsson School of Computer Science and Information Technology The University of Nottingham nhn@cs.nott.ac.uk 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 (5)
-
Arie Peterson -
Daniel McAllansmith -
Henrik Nilsson -
Neil Mitchell -
S. Alexander Jacobson