Hi
Bruno Oliveira wrote:
> Hi Frank!
>
> But then I have a paradox ...
>>>Clearly a misconception of mine.
>
Frank:
>>I'm afraid the misconception is Conor's.
Frank, does it make sense to you to call a logical system `sound' if you
can use it to prove things which aren't true?
I did seek to be cle
Hi folks
Iavor S. Diatchki wrote:
hi,
you can use the reader (environment monad) for this.
lately i have been using 2 combinators to do things like that (thanks to
Thomas Hallgren for showing me this):
-- a nicer name for fmap (or liftM if one prefers)
(#) :: Functor f => (a -> b) -> f a -> f b
Hello Oleg, hello all
I agree with you on this:
[EMAIL PROTECTED] wrote:
There is a view that in order to gain static assurances such as an
array index being always in range or tail being applied to a
non-empty list, we must give up on something significant: on data
structures such as arrays (to be
Hello again
Me:
What if I don't trust your kernel?
[..]
What's the downloadable object that can be machine-checked to satisfy
my paranoid insurance company?
Oleg:
I hope that you can forgive me if I reply by
quoting the above two paragraphs back to you, with the substitution
s/kernel/compiler/.
Hi Martin
Martin Sulzmann wrote:
Hi,
Inspired by Conor's and Oleg's discussion let's see which
dependent types properties can be expressed in Haskell (and extensions).
I use a very simple running example.
[..]
We'd like to statically guarantee that the sum of the output list
is the sum of the two i
