Hardly. As described in the article `all([])` is equivalent to `?x Fx` or "all unicorns are blue". `any([])` is equivalent to `?x Fx` or "a blue unicorn exists".
This confusion is why explicitly using logical quantifiers is preferable: `exists x. x` is (isomorphic to) the top type (if there is one), and `forall x. x` is (isomorphic to) the bottom type (if there is one).
> Syntax sugar that translates `foo.bar(x, y)` into `bar(foo, x, y)`
For that to be syntactic sugar it would have to be the case that foo.bar(x, y) and bar(foo, x, y) always produce the same result for any given values of 'foo', 'x' and 'y'.
(((x -> _|_) -> _|_) -> x) would be the type of double negative reduction. I'm not entirely sure what the type should be. Perhaps, (((x -> _|_) -> (y, y -> _|_)) -> x) is more accurate. In any case, each of the three types are equivalent.
I wanted:
(forall x. ((~x) -> x) -> x) -> (forall y. y \/ (~y))
If we are defining ANY as an n-element LIST operator, in a programming language, which recursively applies the 2-operand AND taking literal Boolean values, there are no ambiguities.
Note that this is inherently a constructible relation, which avoids many pratfalls of more general mathematics.
But if ANY & ALL are being defined as general mathematical relations over all EXISTING members of a class (whose members’ construction, consistency or completeness, may be unknown or even unattainable), then there are other issues.
This means that X must be different from each of these elements.
More generally, which elements can be dropped at all from the list [a,b,c]:
?- drop(X, [a,b,c], _).
X = a ;
X = b ;
X = c ;
dif(X, c),
dif(X, b),
dif(X, a).
Interestingly, the predicate definition does not even use "=" in its clauses. In Prolog, (=)/2 is a built-in predicate that means unification. In the definition above, we use implicit unification instead of explicit unification.
Prolog implementations provide destructive operations and mutation, but here above this is done with unification only. Arguably, you could say that unification performs mutation (but only once).
You still need a way of normalizing expressions that is consistent with your runtime. To say that types ((x: bool) => F<true && x>) and ((x: bool) => F<false || x>) are the same, wrt judgemental equality, requires normalizing both to ((x: bool) => F<x>).
That's true (and mostly is due to the concrete nature of Bool) but even so, parametricity does help a lot implementing that function. `forall a.` cuts down on possible implementations, but you still gotta program sometimes :)
In a more dependently-typed language, we can write something like this
f1 :: (p :: a -> Bool) -> [a] -> [a `suchThat` p a]
f2 :: (p :: a -> Bool) -> [a] -> [a `suchThat` not (p a)]
and that would make it so f1 couldn't be filterNot and f2 couldn't be filter.
And we get the added benefit of giving the caller of our function the proof that the elements have passed that predicate (maybe they can make use of that downstream)
But even in this case, there's nothing stopping you from just always returning an empty list. Not all theorems come for free!
In MAGMA, a computer algebra programming language, there is a “exists” statement which takes a comprehension and evaluates to true if any item is true, something like exists{x % 2 == 0 for x in numbers}. But it also has an extra parameter which can bind the value of the first item satisfying the condition, something like
If exists(y){x : x % 2 == 0 for x in numbers}:
Print y
There is also a “for all” statement which can return the first offender which does not satisfy the condition.
It’s an awkward but incredibly useful language choice - it would be interesting to see it explored more in mainstream languages.
reply