I would make the 'type' symbol a single character ala Agda. For example, a : Int
If your users are writing a lot of types, make it easy! On Dec 22, 2011 10:42 AM, "Alexander Solla" <alex.so...@gmail.com> wrote: > > > 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 > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe