Re: [Haskell-beginners] Using a concept from Category Theory to enable you to come back home after your function has taken you somewhere
Hi Miguel, First note that I am very much a beginner at Category Theory. I am just sharing what I learn.
How do you know that a Haskell function is injective? I don't think it's possible to write a function which checks if another function is injective or not .
A function is injective if each input value (domain) yields a different output value (codomain). So if the set of inputs is finite, then it should be possible to write a function that loops over each input value and checks that its output is distinct from all other outputs.
How to automatically get the inverse of a Haskell function?
That's a great question. I don't know the answer to that. Anyone else have an idea? /Roger
On Sat, Aug 04, 2012 at 05:59:59PM +0000, Costello, Roger L. wrote:
How to automatically get the inverse of a Haskell function?
That's a great question. I don't know the answer to that. Anyone else have an idea?
It is not possible in general... but on the other hand you can use parametricity to pull some cool tricks. See Janis Voigtländer's paper from 2009, "Bidirectionalization for free!" (http://www.iai.uni-bonn.de/~jv/popl09-2.pdf) which is a fun read. You can even play with an implementation of it here: http://www-ps.iai.uni-bonn.de/cgi-bin/bff.cgi -Brent
Hi Roger, A 04/08/2012, às 18:59, Costello, Roger L. escreveu:
Hi Miguel,
First note that I am very much a beginner at Category Theory. I am just sharing what I learn.
Yes I understand that, but what I was trying to say is that I don’t think that this is much related with category theory.
How do you know that a Haskell function is injective? I don't think it's possible to write a function which checks if another function is injective or not .
A function is injective if each input value (domain) yields a different output value (codomain). So if the set of inputs is finite, then it should be possible to write a function that loops over each input value and checks that its output is distinct from all other outputs.
Yes, but very few functions have finite domains, and if they do and it’s big it would take a long time to test it. That is not a technique that can be used in practice I think. Brent wrote:
It is not possible in general... but on the other hand you can use parametricity to pull some cool tricks. See Janis Voigtländer's paper from 2009, "Bidirectionalization for free!" (http://www.iai.uni-bonn.de/~jv/popl09-2.pdf) which is a fun read. You can even play with an implementation of it here:
http://www-ps.iai.uni-bonn.de/cgi-bin/bff.cgi
-Brent
Yes, I think that was the paper I had seen. Interesting stuff. best, Miguel Negrão
participants (3)
-
Brent Yorgey -
Costello, Roger L. -
Miguel Negrao