On Tue, Dec 20, 2011 at 10:30 PM, Gregory Crosswhite
<gcrosswh...@gmail.com>wrote:
>
> On Dec 21, 2011, at 2:24 PM, Alexander Solla wrote:
>
> I would rather have an incomplete semantic, and have all the incomplete
> parts collapsed into something we call "bottom". We can then be smart and
> stay within a total fragment of the language (where bottom is guaranteed to
> not occur).
>
>
> But part of the whole point of including bottom in our semantics in the
> first place is *exactly* to *enable* us to be smart enough to know when we
> are staying within a total fragment of the language. For example,
> including bottom in our semantics allows us to make and prove statements
> like
>
> fst (42,_|_) = 42
>
A proof:
fst :: (a,a) -> a
fst (a,b) = a
and
>
> fst _|_ = _|_
>
This expression is basically non-sense. Should we accept
straight-forwardly ill-typed expressions like:
data Strict a = Strict !a
fst (Strict [1..])
just because the argument is "strictly" a bottom? Bottom inhabits every
type, but only vacuously.
To be generous in my interpretation, I assume you mean something like:
fst (_|_, 10) = _|_.
That is still proved by
fst (x,y) = x
Things like seq, unsafeCoerce, and the like, are defined as (functions
into) bottom in GHC.Prim, and the real semantic-changing magic they perform
is done behind the scenes. It cannot be expressed as Haskell in the same
Haskell context it is used. So assuming you mean something like:
fst (seq [1..] (1,2))
I must respond that you are using one of these magical keywords which
change Haskell's semantics. They should be avoided.
>
> Refusing to use bottom in our semantics doesn't make life better by
> forcing us to stay within a total fragment of the language, it actually
> makes life harder by removing from us a useful tool for knowing *how* to
> stay within a total fragment of the language.
>
I am collapsing the semantics for "distinct" bottoms into a single bottom
and noting that it has no interpretation as a Haskell value.
Notice that this brings Haskell's type theory in line with ZF and typed set
theories. In those theories, bottom merely exists as a syntactic
expression with no interpretation. It is the proto-value which is not
equal to itself. We can say that it inhabits every type. But that is only
vacuously. Bottom does not exist.
We can stay in the total fragment of Haskell very easily, essentially by
using my quotient construction for bottom:
http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html
It requires a shift of point of view, from denotational semantics and
"computational effects" (the things we're trying to avoid by going
functional and lazy!) to the language of logic, proof, and interpretation.
It is possible, consistent, and much simpler conceptually and in use.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
