Lennart Augustsson wrote (on Sat, 14 May 2005 at 16:01):
Why would a constructivist think that all functions are continuous?
It makes no sense.
How would you define a non-continuous function (on reals, say)
without (something like) definition by undecidable cases?
Formal systems
Greg Buchholz wrote (on Wed, 09 Mar 2005 at 20:08):
Can anyone recommend a nice dependently typed language to play with?
Cayenne, Epigram, other?
http://www.cs.chalmers.se/~catarina/agda/
See also the sexy IDE alfa: http://www.cs.chalmers.se/~hallgren/Alfa/
Peter Hancock
Lennart Augustsson wrote (on Mon, 14 Feb 2005 at 14:55):
Any definition can be made point free if you have a
complete combinator base at your disposal, e.g., S and K.
Haskell has K (called const), but lacks S. S could be
defined as
spread f g x = f x (g x)
Ben Rudiak-Gould wrote (on Tue, 25 Jan 2005 at 14:49):
Mark Carroll wrote:
Wasn't there someone mentioning here a little while ago
some project where they strip most of System.* from the libraries and get
something that might be suitable for embedded applications? What was
Jon Cast wrote (on Tue, 14 Dec 2004 at 22:02):
No. All that is needed for ($) to work is impredicativity (or, more
precisely, for the foralls in ($)'s type to be impredicative). That is
something that could easily be implemented in a compiler. I'm not clear
on why it
At the moment I'm only thinking of parameter-less kind declarations but
one could easily imagine kind parameters, and soon we'll have kind
polymorphism but one step at a time.
Any thoughts?
Apologies if it's widely known, but a system with kind polymorphism
was first considered by
Sound on linux tends to center around the jack sound
architecture. This is a demon for connecting audio and midi gadgets
as it were by jack-leads. From a brief look, it seems very callback
oriented. It seems to be highly thought of by knowledgable audio
types, and the bee's knees for low
Samuel E Moelius, wrote (on Wed, 06 Aug 2003 at 15:35):
On Wednesday, August 6, 2003, at 06:15 AM, C T McBride wrote:
This is why most sensible dependent type theories have a hierarchy of
universes behind the scenes. You can think of * in Haskell as the lowest
universe,
On the hskell list, spj wrote
I forget whether I've aired this on the list, but I'm seriously
thinking = that we should change 'forall' to 'exists' in existential
data constructors
Thanks! It made me wonder what colour the sky is on planet Haskell.
From a Curry-Howard point of view, (I
Andy Moran wrote (on Fri, 26 Jul 2002 at 16:52):
As for removing vowels, instead of proposing a solution, I choose to dispute
that the problem needs solving and claim victory.
Removing vowels from identifiers can be very important if
you are writing in certain assemblers from the
lmichele wrote (on Sun, 30 Jun 2002 at 09:26):
By the way, what's the purpose of this coding? (this is the type of
question: ok, I have a hammer, now, for what kind of nail it is useful?)
I would guess that something like the asked-for counter could be
useful if one is allocating
Apropos of section notation, don't forget flip, alias the C
combinator. It allows you to express partial applications to the next
argument but one is in operator section notation.
We can express (usually horribly) any affine lambda-abstraction with
flip, (.), id and const.
Peter Hancock
12 matches
Mail list logo
