On Wed, 2007-02-07 at 13:08 -0500, Jacques Carette wrote: > skaller wrote: > >> 3) Very cool, especially for the axioms -- when will we see them as part > >> of the typeclass? > >> > > > > I actually tried to put one in but found it was a bit nasty. > > Hmm .. do we have any theoreticians around .. > > > Very nasty, because for non-trivial monads the proof obligations are > quite substantial.
Yes, but mere statement of the laws would be useful, even if they can't be proven and we falsely claim they're all axioms .. might have been better to call them 'laws' than axioms, since that doesn't try to separate axioms from theorems. > I don't think it is theory you need there, it is good proof-tools. I'm looking at Why. It's written in Ocaml, and it isn't a theorem prover but a translator which takes a simple language and translates the obligations into those which can be processed by other tools such as Coq, Simplify, etc.. that would leave a need to (a) translate Felix axioms etc into Why code (b) fill in proofs if necessary (b) can be avoided initially by sticking to use of automatic theorem provers rather than assistants. The idea here isn't proving program, or even typeclass instance correctness, but rather simply proving some typeclass 'axioms' are theorems. Hopefully this reduces the workload to get *some* proof capability into Felix. > >> 4) What about something like 'do' notation, to make programming with > >> Monads easier? > >> > > > > * It's not clear how useful it would be in Felix, since as > > an imperative language it's already running STM monad, > > it has 'goto' so it already has continuation passing .. etc :) > > > And yet I (with 2 co-authors) still felt the need to introduce a nicer > notation for monads in ocaml. > > Note how we use 'perform' and '<--' instead of 'do' and '<-', so as to > not interfere with the ocaml syntax. Well 'perform' and "<--" are not used in Felix so we could use them. > > Some examples would help. > > > Code that uses Maybe (instead of exceptions) rapidly gets unreadable > without some sugar. Same with code in any non-builtin monad. It would be cool is the builtin syntax extension facility could provide this kind of thing. Unfortunately whilst it provides good support for statements, it only provides weak support for expressions: you're stuck with infix and outfix (bracket) extensions. The system is capable of parsing anything with recursive descent, and non-terminals can be introduced and analysed, however adding new kinds of expressions is tricky, not the least because the Ocamlyacc expression grammar has a LOT of productions. The only way to fix this is probably Haskell's solution: remove almost all the productions from the grammar with a large scale terrorist attack to force their reintroduction in the library. > > * one might actually decide to make a swag of existing > > Felix notation sugar for STM monad .. i.e. make the > > core more functional > > > I would certainly like that move - and doing this might allow you to > give better error messages too, because you'd be giving the compiler > more information! Yes, but it may cause massive performance loss, as in GHC, which isn't even close to Felix for simple functional calculations (but everything probably trashes Felix when it comes to lists .. see separate thread on the garbage collector). The problem with this kind of thing is that it is very hard to do incrementally .. i don't much like the idea of a compiler rewrite without at least one other worker. Also not clear that the size of the current user base justifies it.. ;( -- John Skaller <skaller at users dot sf dot net> Felix, successor to C++: http://felix.sf.net ------------------------------------------------------------------------- Using Tomcat but need to do more? Need to support web services, security? Get stuff done quickly with pre-integrated technology to make your job easier. Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642 _______________________________________________ Felix-language mailing list Felix-language@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/felix-language
