Polymorphic self application
I have an example of System F plymorphism that I don't really understand:
If I would remove the types it would remain: \f.\a.f (f a) which makes no sense.
Can you help me with this? Thank you!
Solution
The erased term does make sense: in Haskell it would be \f a -> f (f a), a fairly ordinary function that applies its first argument to its second, and then again to the result.
The difference between \f a -> <body> and \f.\a. <body> is only one of notation. If you prefer, write the Haskell term \f -> \a -> f (f a), which is equivalent but syntactically a bit closer to the erased System F.
(Note that double is not self application, which would be \f -> f f.)
- Why does the implementation of *> return something from the left argument?
- Haskell Illegal term-level use of the type constructor 'Int'
- Resolving ambiguous type variable
- How to stop Haskell Parsec parser at EOF
- Is there a type composition operator in Haskell?
- How to create most generic function possible that applies a function to tuple items
- What is the purpose of Rank2Types?
- How do I install GHC 7.8.1 and assign it a different command?
- Couldn't match type `a' with `STRef s Integer'
- Does the behavior of these two function differ in any way that justifies GHC compiling them down to different object code?
- Plotting a graph using Haskell
- Does GHC allow newtypes to have existential type variables?
- Build Prism path selectively base on values
- Proof of concept in Haskell HUnit Testing
- What determines the the lifetime of the process spawned via System.Process.createProcess?
- Efficient connected components from a 2D array
- Haskell saferead of file
- Why doesn't this program return? Or is it a deadlock?
- Can I use StateT/MaybeT/forever to eliminate explicit recursion from this IO action?
- function that validates an address in Haskell
- cabal run pass arguments to program
- Can I write a dependent left fold in terms of a dependent right fold?
- How can I lazily forward text to shell program and lazily get output back from it?
- Multiplication problem involving kind `Nat`
- How can I extract the base name of a directory with at least one dot in its name?
- Converting IEEE 754 floating point in Haskell Word32/64 to and from Haskell Float/Double
- Liquid Haskell error with binary search tree deletion
- Why can't print text passed via std input to createProcess-ed process?
- Combining "Lens' s a" and "a -> Lens' s b" into a "Lens' s b"
- What constitutes codata in the context of programming?