[Haskell-cafe] Fwd: enhancing type classes with properties

Alberto G. Corona agocorona at gmail.com
Thu Oct 23 17:19:46 EDT 2008


Also in my weblog:
http://haskell-web.blogspot.com/2008/10/axioms-properties-for-haskell-classes.html

2008/10/23 Alberto G. Corona <agocorona at gmail.com>

> 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 <agocorona at gmail.com>
>
> 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 <neil.mitchell.2 at credit-suisse.com>
>>
>>>  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
>>> *<www.credit-suisse.com/emea/legal>*
>>>
>>>
>>>  ------------------------------
>>> *From:* Alberto G. Corona [mailto:agocorona at 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 <neil.mitchell.2 at credit-suisse.com>
>>>
>>>>  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
>>>> *<www.credit-suisse.com/emea/legal>*
>>>>
>>>>
>>>>  ------------------------------
>>>> *From:* haskell-cafe-bounces at haskell.org [mailto:
>>>> haskell-cafe-bounces at haskell.org] *On Behalf Of *Alberto G. Corona
>>>> *Sent:* 22 October 2008 1:43 pm
>>>> *To:* haskell-cafe at 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
>>> ==============================================================================
>>>
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20081023/b4669d60/attachment.htm


More information about the Haskell-Cafe mailing list