[Haskell-cafe] Proof that Haskell is RT

[Mitchell, Neil]

> It's possible that there's some more direct approach that 
> represents types as some kind of runtime values, but nobody 
> (to my knowledge) has done that.

It don't think its possible - I tried it and failed.

Consider:

show (f [])

Where f has the semantics of id, but has either the return type [Int] or
[Char] - you get different results. Without computing the types
everywhere, I don't see how you can determine the precise type of [].

Thanks

Neil

> On Wed, Nov 12, 2008 at 12:39 PM, Luke Palmer 
> <lrpalmer at gmail.com> wrote:
> > On Wed, Nov 12, 2008 at 3:21 AM, Jules Bean 
> <jules at jellybean.co.uk> wrote:
> >> Andrew Birkett wrote:
> >>>
> >>> Hi,
> >>>
> >>> Is a formal proof that the Haskell language is 
> referentially transparent?
> >>>  Many people state "haskell is RT" without backing up 
> that claim.  I 
> >>> know that, in practice, I can't write any counter-examples but 
> >>> that's a bit handy-wavy.  Is there a formal proof that, for all 
> >>> possible haskell programs, we can replace coreferent expressions 
> >>> without changing the meaning of a program?
> >>
> >> The (well, a natural approach to a) formal proof would be 
> to give a 
> >> formal semantics for haskell.
> >
> > Haskell 98 does not seem that big to me (it's not teeny, but it's 
> > nothing like C++), yet we are continually embarrassed about 
> not having 
> > any formal semantics.  What are the challenges preventing its 
> > creation?
> >
> > Luke
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
> >
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
> 

==============================================================================
Please access the attached hyperlink for an important electronic communications disclaimer: 

http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==============================================================================