idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.42k stars 643 forks source link

Inlining: let versus where clauses #3377

Open BartAdv opened 8 years ago

BartAdv commented 8 years ago

Following example shows the behaviour - foo causes unsafePerformIO to be called once, whereas version with where (foo2) calls it two times. Why is that? Can it somehow be controlled (something like 'noinline' if it's inlining issue)?

My motivation for such feature is that I'm attempting a port of Sodium FRP library, and certain trick is needed to have mutable internals and pure user-facing API.

mkFoo : String -> Foo
mkFoo s = unsafePerformIO $ do
  printLn "mk"
  pure $ MkFoo s

foo : String -> (Foo, Foo)
foo s =
  let w = mkFoo s
  in (w, w)

foo2 : String -> (Foo, Foo)
foo2 s = (w,w) where
  w = mkFoo s
ahmadsalim commented 7 years ago

@BartAdv Do you think such thing would be better solved using something like the ST monad?

BartAdv commented 7 years ago

I attempted to use IORefs, which, for a toy implementation and single-threaded IO would behave like an ST, right?:

  do
    let ev = someEvent
    let ev2 = map foo someEvent
    listen ev2 callback

During the call to listen some internal structure needs to be updated to reflect that we're adding a listener to ev2 that will call a callback, and ev2 has a listener to ev that just maps produced value with foo.

The approach I've attempted (used in Haskell Sodium implementation and in Reflex FRP library as well), is to use IORef for this. Each event has an IORef that contains either an IO action to update the internals (sort of a node in a graph), or the internals itself (once the event has been listened to). It can be thought of as a delayed thunk - once executed, it's replaced with the returned value and never executed again. This issue with inlining stops me from using such trick.

BartAdv commented 7 years ago

Just a note: I've managed to workaround my initial issue with some "manual knot tying". I initialize IORef with believe_me and pass that ref to a function that produces the value that's gonna be stored in the IORef in the end).