Copatterns in Idris
github.com
github.com
Honestly, I've always missed defsetf or a similar construct in languages without macros. Python's __setitem__ and __setattr__ are already nicer than C++'s pretense of using references, but setf gives you nice improtvement.
For non-lispers:
In common lisp, if you assign (setf) an expression, the compiler looks for the corresponding setf-method.
As an illustration, consider
ball.roundness() = true;
where the outermost expression is a .roundness() call, which you could transform into
ball.set_roundness(true)
without much confusion.
Note that this is conceptually more complex if you want to do this in a purely-functional language.
How is it different than what's described in the article? I mean, I don't know Idris, have no idea what codata is and only skimmed the article, but the similarity seems obvious.
Roughly, data is of finite size, and codata is of infinite size. Consider a (normal finite) list vs an infinite lazy list.
The standard pattern for working with data is to break it into smaller pieces, using pattern matching, till you hit a base case. In Scheme (hopefully close enough to CL you can read it; and not using pattern matching, but whateva) you write stuff like
(define (foldr f zero lst)
(cond lst
[(null? lst) zero]
[else (f (car lst) (foldr f zero (cdr lst)))]))
Now what about codata? You can't break down infinite data till you hit a base case, because there is no base case. It's infinite! So you apply the Fundamental Theorem of Pretending You Understand Category Theory, and prepend co- to all technical terms in the description for data.
So if data is processed using pattern matching and recursion, then codata is processed using copattern matching and corecursion.
By a strange quirk of fate this actually makes sense. You can read more about corecursion (aka coinduction) on your local Internet, and I guess copatterns, as described in the post, are the next piece of the puzzle.
There is a slight analogy with setf but it doesn't go very far.
HTH.
Seeing the paper at http://www.jucs.org/jucs_10_7/total_functional_programming/j... it's more related to proofs, and indeed Idris seems somewhat similar to Coq (a "programming" language for writing proofs). Or maybe I'm just totally lost.
Actually, I know Scheme much better than CL, so no problem here :)
> So you apply the Fundamental Theorem of Pretending You Understand Category Theory, and prepend co- to all technical terms in the description for data.
That, however, is a bit of a problem...
> There is a slight analogy with setf but it doesn't go very far.
Yup, that's what I had in mind; it really looks similar to setf on the surface. That it's something completely different inside should be obvious from it being Idris, category theory, dependent co-typing and co-everything else I don't understand at all :)
Thanks for the link, I love the blog, will need to read this post.
Very nice.
I'm interested in how various languages handle this, mainly so I can steal ideas for my project Mutagen, a purely functional Pythonic language. I recently added modification operators that behave rather like a nestable setitem/setattr. Basically:
list_of_objects = list_of_objects <- [index].attr = 'abc'
So, incf, which is CL's +=, could be defined as
(defmacro (incf lexpr val) `(setf ,lexpr (+ ,lexpr val))
which would evaluate "lexpr" both as a place to put the new value in and as an expression to get the old value out.
If you wanted to do that in terms of purely-functional monad application, it gets a bit hairier... Basically, you've got things like "+=" which are mutators (i.e. functions Int->Int). And you've got places, which either (i) take an X mutator and turn it into a mutator for Y, or (ii) take a Y and return an X (accessor).
In your example,
list_of_objects[index].attr = 'abc'
would mean that you take a "constant value" mutator that takes some string and returns "abc" and turn it first into a mutator that changes the .attr value of something ... to something that changes the .attr value of index [index] of the list_of_objects member of the current data.
Why would that kind of functional style be useful? Basically, because you could write something like a Python program that still allows for search/nondeterminism/backtracking etc.
Some of the weirdness I see in Mutagen seems to come from a partial (or just differing) understanding of how Python and Haskell, respectively, do things. Shoot me a PM if you want to discuss more.
What you describe is somewhat similar to what I had in mind, but a more well-defined abstraction. I hadn't yet formulated it in terms of types, because for now it's just a hack in the bootstrap interpreter, and anyways a lot of Mutagen's type system is still in my head, waiting to be implemented once I have a better understanding of how/why other functional languages do this stuff.
Haskellers have been at `setf' equivalents for a while now. They call them lenses. (And add the Haskell secret sauce, to generalize setf and mapcar and reduce etc into the same notion.)