Ivan Miljenovic wrote:
On 28 May 2010 15:18, wren ng thornton <w...@freegeek.org> wrote:
Stefan Monnier wrote:
churchedBool :: t -> t -> t
Important detail: the precise type is "∀t. t → t → t".
encodeBool x = \t e -> if x then t else e
So the type of encodeBool should be:
Bool → ∀t. t → t → t
whereas Haskell will infer it to be
∀t. Bool → t → t → t
Those are the same type.
I can see a slight distinction between them, based upon when the
quantification occurs (the former returns a function that work on all
t, the latter will do that encoding for all t).
The isomorphism in System F:
in : (∀t. Bool → t → t → t) → (Bool → ∀t. t → t → t)
in f = \b. /\t. f @t b
out : (Bool → ∀t. t → t → t) → (∀t. Bool → t → t → t)
out g = /\t. \b. g b @t
If you're using the raw System F, then there's a slight difference ---as
there always is between isomorphic things which are non-identical--- but
that difference is not theoretically significant. If you're using a
higher-level language like Haskell, then the conversions are done for
you, so there's even less difference.
The expression 1+1 is distinct from 2: it has a different representation
in memory, it takes a different number of steps to normalize, etc.
Sometimes these differences are important for engineering (e.g., dealing
with space leaks), but they're rarely significant for theory.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
