[Haskell-cafe] Proof that Haskell is RT
neil.mitchell.2 at credit-suisse.com
Wed Nov 12 08:47:59 EST 2008
> 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.
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 .
> 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
Please access the attached hyperlink for an important electronic communications disclaimer:
More information about the Haskell-Cafe