[Haskell-cafe] If you'd design a Haskell-like language, what would you do different?

[Lyndon Maydwell]

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.solla at gmail.com> wrote:

>
>
> On Tue, Dec 20, 2011 at 10:30 PM, Gregory Crosswhite <
> gcrosswhite at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20111222/56493aad/attachment.htm>