Case expressions in STG

[William Knop]

Whoops, looks like my phone dropped Tom from the CC (fixed).

Simon, what about the following:

f = \x -> x
g = \x -> (x,1)
h = \x -> fst (g x)
i = \x -> case f of
  f -> True
  _ -> False

i f => True
i h => ?

If g isn't inlined into h and fst optimized out, wouldn't the head normal form of f and h be different, and the comparison fail even though it shouldn't? Or should it? I've taken function equality to be "f and g are equal iff f x == g x, for all x."

Will


> On Jun 18, 2014, at 7:04 PM, Simon Peyton Jones <simonpj at microsoft.com> wrote:
> 
> I've forgotten what I intended in the STG paper, but GHC's Core language certainly allows case on a function; all it does is to force the function to head normal form.
> 
> Simon
> 
> | -----Original Message-----
> | From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of William
> | Knop
> | Sent: 18 June 2014 23:54
> | To: ghc-devs at haskell.org
> | Subject: Re: Case expressions in STG
> | 
> | Hi Tom,
> | 
> | SPJ is surely more qualified to answer than I, but I'll take a stab.
> | 
> | In general, it is computationally infeasible to compare functions.
> | Granted, in your example, the function isn't being compared-- and
> | therefore the case expr is extraneous. I don't think there exists a
> | feasible, uncontrived example, so I imagine that's why STG forbids it
> | (though I don't know where it's specified).
> | 
> | Cheers,
> | Will
> | 
> | 
> | > On Jun 18, 2014, at 9:43 AM, Tom Ellis <tom-lists-ghc-
> | devs at jaguarpaw.co.uk> wrote:
> | >
> | > I am reading SPJ's seminal work "Implementing lazy functional languages
> | on
> | > stock hardware: the Spinless Tagless G-machine" (1992).  The paper is
> | > available here
> | >
> | >    http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.3729
> | >
> | > On p62 we see "The expression scrutinised by a case expression must
> | > eventually evaluate either to a primitive value or a constructor
> | > application.".
> | >
> | > This doesn't make sense to me.  Isn't the following a valid STG
> | program?
> | > What am I missing?  Where is it specified that the scrutinee of a case
> | > expression cannot be of a function type?
> | >
> | > {x} \n {z} -> let f = \{x} \n {y} -> g x y
> | >              in case f of f' -> f' z
> | >
> | > Thanks,
> | >
> | > Tom
> | > _______________________________________________
> | > ghc-devs mailing list
> | > ghc-devs at haskell.org
> | > http://www.haskell.org/mailman/listinfo/ghc-devs
> | _______________________________________________
> | ghc-devs mailing list
> | ghc-devs at haskell.org
> | http://www.haskell.org/mailman/listinfo/ghc-devs