I am interested in trying to use category to perform some mathematical
computations. It seems natural to want to talk about categories of mathematical objects e.g. Groups,Rings,Algebras ... etc. But I have found some difficulty doing this with Haskell's standard Category libraries. class Category m where id :: m a a comp :: m a b -> m b c -> m a c The main issue is that the objects of the category (represented by the id morphism) are in bijection to some set of haskell types. The problem (I think) this leads too is that 1. All the objects that may appear in a program must be known to the compiler. Which leads to problems (for me at least) as the application I want to study I don't know all the (Groups,Rings,... etc) that I will need. 2. This requires representing (for example) all groups as types. In general I have found while possible it leads to pretty horrendous types. Now this all makes sense Haskell's categories are for reasoning about programs while I want to use it more for pure maths. Has anyone else had a similar problem with categories in haskell? Or am I missing a way of implementing such structures within the standard Category framework for haskell. For a (toy) example take trying to model the category of CyclicGroups --Cyclic n is the object representing the cyclic group Z_n newtype Cyclic = Cyclic Int --CyclicMor n m p is represents a group morphism from Z_n to Z_m taking 1 -> p newtype CyclicMor = CyclicMor Int Int Int This now gives the definition of id :: Cyclic -> CyclicMor id (Cyclic n) = CyclicMor n n 1 comp :: CyclicMor -> CyclicMor -> Maybe CyclicMor comp (CyclicMor n m p) (CyclicMor n' m' p') | m==n' = Just (CyclicMor n m' (p+p')) | otherwise = Nothing The main loss in this approach is compiler can no longer determine if morphisms are compatible. In my project I use a slightly more generic variant : class OrdinaryCategory m where id :: a -> m a a comp :: m a b -> m b c -> Maybe (m a c) I haven't seen a similar construction in haskell libraries does anyone know if this is because 1. It is already there and I just haven't come across it. 2. It solves a problems that no-one else has had. 3. My idea is fundamentally broken / useless in some key way. Thanks for any comments anyone has. Robert -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/beginners/attachments/20130529/d268eeca/attachment.htm> |
Robert Goss <goss.robert at gmail.com> wrote:
> The main issue is that the objects of the category (represented by > the id morphism) are in bijection to some set of haskell types. > > [...] > > Now this all makes sense Haskell's categories are for reasoning about > programs while I want to use it more for pure maths. Has anyone else > had a similar problem with categories in haskell? Or am I missing a > way of implementing such structures within the standard Category > framework for haskell. Perhaps what you need is not a programming language like Haskell, but a proof assistant like Agda, where you can express arbitrary categories. A limited form of this is possible in Haskell as well, but the lack of dependent types would force you through a lot of boilerplate and heavy value/type/kind lifting. Greets, Ertugrul -- Not to be or to be and (not to be or to be and (not to be or to be and (not to be or to be and ... that is the list monad. -------------- next part -------------- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 836 bytes Desc: not available URL: <http://www.haskell.org/pipermail/beginners/attachments/20130529/7c9ac314/attachment.pgp> |
On 29 May 2013 22:04, Ertugrul S?ylemez <es at ertes.de> wrote:
> > > Perhaps what you need is not a programming language like Haskell, but a > proof assistant like Agda, where you can express arbitrary categories. > A limited form of this is possible in Haskell as well, but the lack of > dependent types would force you through a lot of boilerplate and heavy > value/type/kind lifting. > > I had had a look at Agda a while ago I will have to have another look. How possible is it to do computations in Agda? For example is it possible to compute the equalizer of 2 arrows (obv is a category in which equalizers exit)? A part of this was a learning experience it seemed natural to express certain bits of computer algebra in terms of categories and I wanted to see how well these ideas could be expressed in haskell. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/beginners/attachments/20130529/5b696d69/attachment.htm> |
I haven't tried Idris yet myself, and I'm not sure how stable it is, but I
think it can do a lot that Agda can do but more suitable for actual calculations. I would be interested to hear any experiences you have (or have had) with it. Peter On 29 May 2013 23:11, Robert Goss <goss.robert at gmail.com> wrote: > > > > On 29 May 2013 22:04, Ertugrul S?ylemez <es at ertes.de> wrote: > >> >> >> Perhaps what you need is not a programming language like Haskell, but a >> proof assistant like Agda, where you can express arbitrary categories. >> A limited form of this is possible in Haskell as well, but the lack of >> dependent types would force you through a lot of boilerplate and heavy >> value/type/kind lifting. >> >> > I had had a look at Agda a while ago I will have to have another look. How > possible is it to do computations in Agda? For example is it possible to > compute the equalizer of 2 arrows (obv is a category in which equalizers > exit)? > > A part of this was a learning experience it seemed natural to express > certain bits of computer algebra in terms of categories and I wanted to see > how well these ideas could be expressed in haskell. > > _______________________________________________ > Beginners mailing list > Beginners at haskell.org > http://www.haskell.org/mailman/listinfo/beginners > > An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/beginners/attachments/20130530/440b65f8/attachment.htm> |
I've heard a talk about Idris last weekend at BerlinSides. Looks very
interesting - I think I'll have to take a closer look at it. The guy said it isn't stable enough for productive use but as Robert asked for some learning experiences, this should be interessting for him, too. ( Btw: there should be four (?) video lectures about Idris somewhere at http://idris-lang.org/ ) Friedrich 2013/5/30 Peter Hall <peter.hall at memorphic.com>: > I haven't tried Idris yet myself, and I'm not sure how stable it is, but I > think it can do a lot that Agda can do but more suitable for actual > calculations. I would be interested to hear any experiences you have (or > have had) with it. > > Peter > > > On 29 May 2013 23:11, Robert Goss <goss.robert at gmail.com> wrote: >> >> >> >> >> On 29 May 2013 22:04, Ertugrul S?ylemez <es at ertes.de> wrote: >>> >>> >>> >>> Perhaps what you need is not a programming language like Haskell, but a >>> proof assistant like Agda, where you can express arbitrary categories. >>> A limited form of this is possible in Haskell as well, but the lack of >>> dependent types would force you through a lot of boilerplate and heavy >>> value/type/kind lifting. >>> >> >> I had had a look at Agda a while ago I will have to have another look. How >> possible is it to do computations in Agda? For example is it possible to >> compute the equalizer of 2 arrows (obv is a category in which equalizers >> exit)? >> >> A part of this was a learning experience it seemed natural to express >> certain bits of computer algebra in terms of categories and I wanted to see >> how well these ideas could be expressed in haskell. >> >> _______________________________________________ >> Beginners mailing list >> Beginners at haskell.org >> http://www.haskell.org/mailman/listinfo/beginners >> > > > _______________________________________________ > Beginners mailing list > Beginners at haskell.org > http://www.haskell.org/mailman/listinfo/beginners > |
Hi Friedrich,
video lectures and slides of Idris http://edwinb.wordpress.com/2013/03/15/idris-course-at-itu-slides-and-video/ -Mukesh On Thu, May 30, 2013 at 12:20 PM, Friedrich Wiemer < friedrichwiemer at gmail.com> wrote: > I've heard a talk about Idris last weekend at BerlinSides. Looks very > interesting - I think I'll have to take a closer look at it. The guy > said it isn't stable enough for productive use but as Robert asked for > some learning experiences, this should be interessting for him, too. > ( Btw: there should be four (?) video lectures about Idris somewhere > at http://idris-lang.org/ ) > > Friedrich > > 2013/5/30 Peter Hall <peter.hall at memorphic.com>: > > I haven't tried Idris yet myself, and I'm not sure how stable it is, but > I > > think it can do a lot that Agda can do but more suitable for actual > > calculations. I would be interested to hear any experiences you have (or > > have had) with it. > > > > Peter > > > > > > On 29 May 2013 23:11, Robert Goss <goss.robert at gmail.com> wrote: > >> > >> > >> > >> > >> On 29 May 2013 22:04, Ertugrul S?ylemez <es at ertes.de> wrote: > >>> > >>> > >>> > >>> Perhaps what you need is not a programming language like Haskell, but a > >>> proof assistant like Agda, where you can express arbitrary categories. > >>> A limited form of this is possible in Haskell as well, but the lack of > >>> dependent types would force you through a lot of boilerplate and heavy > >>> value/type/kind lifting. > >>> > >> > >> I had had a look at Agda a while ago I will have to have another look. > How > >> possible is it to do computations in Agda? For example is it possible to > >> compute the equalizer of 2 arrows (obv is a category in which equalizers > >> exit)? > >> > >> A part of this was a learning experience it seemed natural to express > >> certain bits of computer algebra in terms of categories and I wanted to > see > >> how well these ideas could be expressed in haskell. > >> > >> _______________________________________________ > >> Beginners mailing list > >> Beginners at haskell.org > >> http://www.haskell.org/mailman/listinfo/beginners > >> > > > > > > _______________________________________________ > > Beginners mailing list > > Beginners at haskell.org > > http://www.haskell.org/mailman/listinfo/beginners > > > > _______________________________________________ > Beginners mailing list > Beginners at haskell.org > http://www.haskell.org/mailman/listinfo/beginners > An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/beginners/attachments/20130530/3de7a676/attachment.htm> |
Free forum by Nabble | Edit this page |