> > min2 :: [a] -> a
> > min2 ((l:ls) :: [a] <= Sorted) = l
> > min2 l = min l
>
> What's the semantics of that supposed to be?
> If the list is not known to be definitely sorted,
> will it check sortedness at runtime?
No.
> If not, then the semantics could be nondeterministic,
> in general, so
On 20-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
> [Lennart wrote:]
> > [Nick Kallen wrote:]
> > > To what
> > > extent will a program that type checks completely fail to follow its
> > > specification? Can someone give specific examples?
> >
> > It's trivial to construct examples. Take sor
What is the general consensus on views and the extended pattern guards that
are discussed at
http://www.haskell.org/development/ ?
I think views are really neat, but am not quite sure how I feel about
pattern guards.
On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> [Fergus wrote:]
> > Well, yes, up to a point, but it may be clearer if the simple
> > regular types part is kept separate from the undecidable part,
> > as was done in NU-Prolog, or as is done in Eiffel.
>
> I'm not necesssarily ad
On 20-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
> [Fergus wrote:]
> > If your language supports optional dynamic type checking, as it should,
> > then expressing functions like apply shouldn't be too hard.
>
> Here's a dynamic apply in a pseudo Clean 2.0 syntax:
>
> apply :: Dynamic [a] -
On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> > (i.e., you leave out the pivot [x])
> >
> > Obviously the result of sort will no longer be a permutation of its
> > argument. Will this then not type check?
>
> No, the proof (whereever it is) would no longer type check.
As I u
On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> > > > F a * = member (map (F a) [0..]) // member [a] a -> Bool
> > > I mave no clue what this means. What is `member'?
> >
> > Member is memq, in, etc. Checks for membership in a list.
> I'm still lost. What is // and how does i
> ...I thought about this pretty hard. Particularly I thought about using
> classes; this was fruitless. So I decided I'd invent a new language feature
> and a nice little syntax to handle it.
>
> Sorted l r = Ordered r /\ Permutation l r
>
> sort :: (l :: [a]) -> (r :: [a]) <= Sorted l r
You'v
We apologize if you receive more than one copy of this message.
COORDINATION '99
http://www.cs.unibo.it/~coord99/
Third Int. Conference on Coordination Models a
[EMAIL PROTECTED] wrote:
> > enabling types to express all properties you want is, IMO, the right way.
>
> Why do I feel that there must be another approach to programming?
>
> How many people do you expect to program in Haskell once you are done adding all
> it takes to "express all imaginable
> I consider even the second one to be mixing the proofs
> with the code, because there's no easy way that I can tell at
> a glance that `sortReallySorts' is a proof rather than a program.
But I consider that a feature and not a bug. :-)
-- Lennart
> > No, the proof (whereever it is) would no longer type check.
>
> As I understand it, this is not necessarily true:
> if the proof contains loops, it might type check,
> even though it is not really a valid proof.
You're right. If the proof is looping it will still
pass as a proof.
-- L
> I believe "//" here is a C++/Java/C9X-style comment.
> Just read it as if "//" were "--". Everything from
> the "//" until the end of line is a comment.
Wow! That's it. Since (//) is an operator on arrays
in Haskell I was trying to make sense out of it, and
failed miserably. :-)
--
> > apply :: (F a *) [a] -> (F a *)
> > apply f [] = a
> > apply f [a:as] = apply (f a) as
> >
> > The type gets noisier.
>
> (To correct a couple of minor typos, that should be
> apply f [] = f
> apply f (a:as) = apply (f a) as
> )
Heh, thank you. :)
> I agree it is in some sense si
> If you return the same proof of correctness that you used
> for the earlier definition of sort, then no it won't type check.
> But if you return a proof defined as e.g.
>
> proof = proof
>
> then if I understand things correctly it will type check.
On that note, since this has been of i
15 matches
Mail list logo
