Re: [Haskell-cafe] Fwd: enhancing type classes with properties
It seems that some of the goals are not so hard. here I publised my
progress.
http://docs.google.com/Doc?id=dd5rm7qq_165rshp74gf&pli=1
I show how to define a Ring, such a mathematical structure in Haskell, how
to instantiate the class Num as a Ring , how to (possibly in other moment of
space-time) instantiate a new class as Num and how to test the axioms for
the new class.
All of then is something like a sophisticated "assert" mechanism, but , I
think, much more flexible and elegant.
2008/10/22 Alberto G. Corona
I guess that the namespace thing is not necesary. Maybe it can be done in template haskell. I never used TH however. it is a matter of inserting code here and there and rewrite rules somewhere at compile time. It´s a nice project. I´ll try.
2008/10/22 Mitchell, Neil
Hi Alberta,
It's a lot of work, but I wish you luck :-) Many of the underlying tools exist, but there definately needs more integration.
Thanks
Neil
This material is sales and trading commentary and does not constitute investment research. Please follow the attached hyperlink to an important disclaimer *
* ------------------------------ *From:* Alberto G. Corona [mailto:agocorona@gmail.com] *Sent:* 22 October 2008 4:23 pm *To:* Mitchell, Neil *Subject:* Re: [Haskell-cafe] Fwd: enhancing type classes with properties
Hi Neil,
I see the contract type mechanism and safety check techniques reflected in the above paper are a good step, But I think that something more general would be better. What I propose is to integrate directly in the language some concepts and developments that are already well know to solve some common needs that I thing can not be solved without this integration:
To make use of:
-Quickcheck style validation. By the way, Don Steward recommend to add quckcheck rules close to the class definitions just for better documentation
- Implicit class properties defined everywhere in the documentation but impossible to reflect in the code (for example the famous monad rules: return x >>= f == f x etc )
- The superb ghc rewrite rule mechanism (perhaps with enhancements)
- object style namespaces, depending on class names.
To solve problems like
- code optimization
- code verification. regression tests for free!!
- The need for safe overloading of methods and operators (making the namespaces dependent not only on module name but also in class names) . Why I can not overload the operator + in the context of a DSL for JavaScript generation if my operator does what + does?
- strict and meaningful rules for class instances. - to make the rewrite rule mechanism visible to everyone
2008/10/22 Mitchell, Neil
Hi Alberto,
Take a look at ESC/Haskell and Sound Haskell, which provide mechanisms for doing some of the things you want. I don't think they integrate with type classes in the way you mention, but I think that is just a question of syntax.
http://www.cl.cam.ac.uk/~nx200/ http://www.cl.cam.ac.uk/%7Enx200/
Thanks
Neil
This material is sales and trading commentary and does not constitute investment research. Please follow the attached hyperlink to an important disclaimer *
* ------------------------------ *From:* haskell-cafe-bounces@haskell.org [mailto: haskell-cafe-bounces@haskell.org] *On Behalf Of *Alberto G. Corona *Sent:* 22 October 2008 1:43 pm *To:* haskell-cafe@haskell.org *Subject:* [Haskell-cafe] Fwd: enhancing type classes with properties
I´m just thinking aloud, but, because incorporating deeper mathematics concepts has proven to be the best solution for better and more flexible programming languages with fewer errors, I wonder if raising the type classes incorporating axioms can solve additional problems.
At first sight it does:
class Abelian a where (+) :: a -> a -> a property ((+))= a+b == b+a
this permits: 1- safer polimorphism: I can safely reuse the operator + if the type and the property is obeyed. The lack of ability to redefine operators is a problem for DSLs that must use wreid symbols combinations with unknow meanings. To use common operators with fixed properties is very good. the same aplies for method names.
2- the compiler can use the axions as rewrite rules.
3- in debugging mode, it is possible to verify the axiom for each value a generated during execution. Thus, a generator is not needed like in quickcheck. The logic to quickcheck can be incorporated in the debugging executable.
3 guaranties that 1 and 2 are safe.
a type class can express a relation between types, but it is not possible to define relation between relations.
============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
Also in my weblog:
http://haskell-web.blogspot.com/2008/10/axioms-properties-for-haskell-classe...
2008/10/23 Alberto G. Corona
It seems that some of the goals are not so hard. here I publised my progress.
http://docs.google.com/Doc?id=dd5rm7qq_165rshp74gf&pli=1
I show how to define a Ring, such a mathematical structure in Haskell, how to instantiate the class Num as a Ring , how to (possibly in other moment of space-time) instantiate a new class as Num and how to test the axioms for the new class.
All of then is something like a sophisticated "assert" mechanism, but , I think, much more flexible and elegant.
2008/10/22 Alberto G. Corona
I guess that the namespace thing is not necesary. Maybe it can be done in
template haskell. I never used TH however. it is a matter of inserting code here and there and rewrite rules somewhere at compile time. It´s a nice project. I´ll try.
2008/10/22 Mitchell, Neil
Hi Alberta,
It's a lot of work, but I wish you luck :-) Many of the underlying tools exist, but there definately needs more integration.
Thanks
Neil
This material is sales and trading commentary and does not constitute investment research. Please follow the attached hyperlink to an important disclaimer *
* ------------------------------ *From:* Alberto G. Corona [mailto:agocorona@gmail.com] *Sent:* 22 October 2008 4:23 pm *To:* Mitchell, Neil *Subject:* Re: [Haskell-cafe] Fwd: enhancing type classes with properties
Hi Neil,
I see the contract type mechanism and safety check techniques reflected in the above paper are a good step, But I think that something more general would be better. What I propose is to integrate directly in the language some concepts and developments that are already well know to solve some common needs that I thing can not be solved without this integration:
To make use of:
-Quickcheck style validation. By the way, Don Steward recommend to add quckcheck rules close to the class definitions just for better documentation
- Implicit class properties defined everywhere in the documentation but impossible to reflect in the code (for example the famous monad rules: return x >>= f == f x etc )
- The superb ghc rewrite rule mechanism (perhaps with enhancements)
- object style namespaces, depending on class names.
To solve problems like
- code optimization
- code verification. regression tests for free!!
- The need for safe overloading of methods and operators (making the namespaces dependent not only on module name but also in class names) . Why I can not overload the operator + in the context of a DSL for JavaScript generation if my operator does what + does?
- strict and meaningful rules for class instances. - to make the rewrite rule mechanism visible to everyone
2008/10/22 Mitchell, Neil
Hi Alberto,
Take a look at ESC/Haskell and Sound Haskell, which provide mechanisms for doing some of the things you want. I don't think they integrate with type classes in the way you mention, but I think that is just a question of syntax.
http://www.cl.cam.ac.uk/~nx200/ http://www.cl.cam.ac.uk/%7Enx200/
Thanks
Neil
This material is sales and trading commentary and does not constitute investment research. Please follow the attached hyperlink to an important disclaimer *
* ------------------------------ *From:* haskell-cafe-bounces@haskell.org [mailto: haskell-cafe-bounces@haskell.org] *On Behalf Of *Alberto G. Corona *Sent:* 22 October 2008 1:43 pm *To:* haskell-cafe@haskell.org *Subject:* [Haskell-cafe] Fwd: enhancing type classes with properties
I´m just thinking aloud, but, because incorporating deeper mathematics concepts has proven to be the best solution for better and more flexible programming languages with fewer errors, I wonder if raising the type classes incorporating axioms can solve additional problems.
At first sight it does:
class Abelian a where (+) :: a -> a -> a property ((+))= a+b == b+a
this permits: 1- safer polimorphism: I can safely reuse the operator + if the type and the property is obeyed. The lack of ability to redefine operators is a problem for DSLs that must use wreid symbols combinations with unknow meanings. To use common operators with fixed properties is very good. the same aplies for method names.
2- the compiler can use the axions as rewrite rules.
3- in debugging mode, it is possible to verify the axiom for each value a generated during execution. Thus, a generator is not needed like in quickcheck. The logic to quickcheck can be incorporated in the debugging executable.
3 guaranties that 1 and 2 are safe.
a type class can express a relation between types, but it is not possible to define relation between relations.
============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================
participants (1)
-
Alberto G. Corona