Re: proving the monad laws
Hello! > Would it be possible to write a piece of Haskell code which checks > the monadic laws automatically by simulating evaluation in this way? To some extent, yes. The proof in the previous message was based on normalization, with respect to associative laws and some betas. So we can take (st f) . (st g) and do: - inlining of the 'st' operation - de-sugaring into core Haskell - more inlining and beta [perhaps to a certain depth] - rearranging expression based on associative laws, e.g., converting f . (g . h) into (f . g) . h converting case (case x of P -> A) of P' -> A' into case x of P -> case A of P' -> A' Then do the same for (st ((st f) . g)) and compare the results. If the results are identical, great. Otherwise, the user has to look at the results and decide if they are the same based on his intuition. GHC already does inlining, de-sugaring, and some betas. I think there is a flag that makes GHC dump the result of these operations for normalization with respect associative laws. BTW, GHC accepts user-defined rules: so we can express associativity rules for known operations and direct GHC to normalize terms with respect to these laws. I don't know how to express side conditions though (e.g., the normalization of 'case' above is valid only if the variables bound by pattern P do not occur in P', A'). It would be great if there was a RULES-pragma operation to alpha-rename bound variables in a term. In that case, we can safely normalize more expressions. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Fundep & Datatype Request
OK, this is an issue I have raised before I think, but I don't remember
what the opinion on it was. The following doesn't compile with ghc
-fglasgow-exts (or Hugs -98):
-- ghc -fglasgow-exts -c TypeLambda.hs
module TypeLambda where
{
class Fc a b | a -> b;
instance Fc Bool Int;
data F1 a = forall b. (Fc a b) => MkF1 b;
makeF1 :: Int -> F1 Bool;
makeF1 = MkF1;
getF1 :: F1 Bool -> Int;
getF1 (MkF1 i) = i;
data F2 a = MkF2 (forall b. (Fc a b) => b);
makeF2 :: Int -> F2 Bool;
makeF2 i = MkF2 i;
getF2 :: F2 Bool -> Int;
getF2 (MkF2 i) = i;
}
Clearly makeF1 and getF2 are OK. But I claim getF1 and makeF2 should
compile, since the type inside either an "F1 Bool" or an "F2 Bool" must
always be an Int. Instead I get this:
TypeLambda.hs:14:
Inferred type is less polymorphic than expected
Quantified type variable `b' is unified with `Int'
When checking an existential match that binds
i :: b
and whose type is F1 Bool -> Int
In the definition of `getF1': getF1 (MkF1 i) = i
TypeLambda.hs:19:
Cannot unify the type-signature variable `b' with the type `Int'
Expected type: b
Inferred type: Int
In the first argument of `MkF2', namely `i'
In the definition of `makeF2': makeF2 i = MkF2 i
So why is this useful? Because you can do some form of type-lambda with
it. For instance, you might have some system of collection types:
Word8 -->> UArray Int Word8
Word16-->> UArray Int Word16
(a -> b) -->> Array Int (a -> b)
It would be nice to hide the implementation and just expose some
type-constructor:
MyCollection Word8
MyCollection Word16
MyCollection (a -> b)
I believe this can't be done currently.
--
Ashley Yakeley, Seattle WA
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
unary minus
Hi,
I wonder why Haskell only allows the unary minus on the left side of an
expression ("lexp" in the grammar).
There should be no problem to uniquely recognize an unary minus right
beside an operation symbol ("qop"). Does the grammar allow two
consecutive qops in other cases?
This would allow "1 * - 1" to be correct (which I think is sort of
"standard"), while "1 - 1" clearly is the infix minus.
What was the rational for the current restriction of the unary minus? Do
I oversee something?
Christian
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: Haskell for non-Haskell's sake
On Thu, 4 Sep 2003, John Hughes wrote: > I wrote the system for my (Haskell!) programming course, with 170 students > last year, and it is now also being used (at least) for our Java course > and a cryptography course. It consists of about 600 lines of Haskell and > 18 lines of C. Just curious. What was C used for? /One of the students in the mentioned haskell programming course... -- | Sebastian Sylvan | | ICQ: 44640862 | | Tel: 073-6818655 / 031-812 817| || || | Hard Work Often Pays Off After Time| | But Laziness Always Pays Off Now! | ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Haskell for non-Haskell's sake
I use Haskell and Wash/CGI for administering students lab work. Students solve programming exercises in pairs, register their pair, and upload their solution over the web. The pair gets a "home page" on which they can see their grade and comments from their tutor, and also submit new solutions if their tutor is unhappy with the first. Tutors have a home page on which they can see which assignments they still need to mark, download the student's code, set grades and enter comments, and also view a summary of results for all students they are responsible for. As the administrator, I can see results for each student, which submissions are waiting to be marked, what the success rate is, and so on. (The administrator's interface is a bit cruder than the other two, since I can always hack the code when I need some more information...). The system also packages up all submitted solutions ready for submission to an automated plagiarism detector. The benefits of the system are that students, tutors, and the administrator can work from any machine on the Internet -- for example, at home; submission and returns are quicker and easier for both students and tutors, so feedback is quicker; tutors and the administrator have a much better overview of the state of students' work; solutions are kept in a uniform form which makes automated cheat detection easy. I wrote the system for my (Haskell!) programming course, with 170 students last year, and it is now also being used (at least) for our Java course and a cryptography course. It consists of about 600 lines of Haskell and 18 lines of C. John Hughes ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: need some info/help
Brett G. Giles wrote: Naturally, there are many great resources for this at www.haskell.org Ensure you check out both Alex and Happy for the parsing and sourcing. (note that Alex is currently being re-written, I'm not sure if the latest public version has the new format/syntax) I think, parsing (including lexical analysis) is much simpler using only a combinator library like the one from Daan Leijen that is part of the ghc base library: http://www.haskell.org/ghc/docs/latest/html/base/Text.ParserCombinators.Parsec.html Cheers Christian ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: need some info/help
Naturally, there are many great resources for this at www.haskell.org Ensure you check out both Alex and Happy for the parsing and sourcing. (note that Alex is currently being re-written, I'm not sure if the latest public version has the new format/syntax) Also, there are a variety of compiler help tools there such as bases for symbol tables and so forth. An excellent resource for anyone writing a compiler in a functional language is "Modern Compiler Implementation in ML" by Andrew Appel See http://www.cs.princeton.edu/~appel/modern/ml/ for a bit of information. Although it is directed at ML (and Ml-lex and ml-yacc) it has great information about the functional way of approaching this. Finally, note that ML above is not a pure functional language. As such, you do get to (cheat and use :) state. I have found that I've needed a variety of state monads while doing compiler writing in Haskell. Good luck and have fun. > Hi > > I know there is a general consensus about finding out new things to use > with Haskell but I am quite a newcomer in this field and am attempting to > write a compiler and a runtime system in Haskell. At this > important juncture I would like to ask for some help with some resources, > books or links which I can look up which would help me understand the > process better. Your help is highly appreciated. > > Thanks :) > ___ > Haskell mailing list > [EMAIL PROTECTED] > http://www.haskell.org/mailman/listinfo/haskell > Brett G. Giles Grad Student, Formal Methods http://www.cpsc.ucalgary.ca/~gilesb mailto:[EMAIL PROTECTED] ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: proving the monad laws
Hello, thank you for the idea of using variables directly to see what happens. This is really a simplification for the proof. At first I thought that there should be a simpler solution and I tried to modify your approach, so that it applies to >>= as well, but now I am convinced :-) I have downloaded the paper of Filinski "Representing Monads" to take a look at the definition directly. It seems to be interesting for me, but deterringly difficult as well :-( Would it be possible to write a piece of Haskell code which checks the monadic laws automatically by simulating evaluation in this way? Maybe a little theoretical section in the monad tutorial which deals with this stuff would be a help as well. Iavor, I am really happy, that this monad is working :-) Never touch a running system or try to make it more difficult as it is! These monad transformers are still a red rag to me. Nevertheless thank you. Ciao, Steffen ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
