On Fri, Dec 30, 2011 at 9:19 AM, Heinrich Apfelmus < apfel...@quantentunnel.de> wrote:
> Conal Elliott wrote: > > Heinrich Apfelmus wrote: >> >> The function >>> >>> f :: Int -> IO Int >>> f x = getAnIntFromTheUser >>= \i -> return (i+x) >>> >>> is pure according to the common definition of "pure" in the context of >>> purely functional programming. That's because >>> >>> f 42 = f (43-1) = etc. >>> >>> Put differently, the function always returns the same IO action, i.e. the >>> same value (of type IO Int) when given the same parameter. >>> >>> >> Two questions trouble me: >> >> How can we know whether this claim is true or not? >> >> What does the claim even mean, i.e., what does "the same IO action" mean, >> considering that we lack a denotational model of IO? >> > > I think you can put at least these troubles to rest by noting that f 42 > and f (43-1) are intentionally equal, even though you're not confident > on their extensional meaning. > > The idea is to represent IO as an abstract data type > > type IO' a = Program IOInstr a > > data Program instr a where > Return :: a -> Program instr a > Then :: instr a -> (a -> Program instr b) -> Program instr b > > instance Monad (Program instr) where > return = Return > (Return a) >>= g = g a > (i `Then` f) >>= g = i `Then` (\x -> f x >>= g) > > date IOInstr a where > PutChar :: Char -> IOInstr () > GetChar :: IOInstr Char > etc... > > So, two values of type IO' a are equal iff their "program codes" are > equal (= intensional equality), and this is indeed the case for f 42 and > f (43-1) . Therefore, the (extensional) interpretations of these values by > GHC are equal, too, even though you don't think we know what these > interpretations are. > > (Of course, programs with different source code may be extensionally > equal, i.e. have the same effects. That's something we would need a > semantics of IO for.) > How do you know that GHC's (or YHC's, etc) interpretation of IO is a composition of this program code interpretation with some other (more extensional) interpretation? In particular, how do you know that no IO primitive can ever distinguish between 42 and 43-1. - Conal
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
