Re: [Camllist] LambdaTerm (f x) (x f) translated to Ocaml?
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Marius Nita <marius@c...> 
Subject:  Re: [Camllist] LambdaTerm (f x) (x f) translated to Ocaml? 
yoann padioleau wrote: >> Hello, >> >> I'm not firm in lambda calculus, what is the lambdaterm >> in the subject translated to OCaml? >> >> Is this possible? > > the ocaml interpreter dont want this definition > > let g f x = (f x) (x f) > > and shout: > this expression has type ('a > 'b) > 'c > 'd but is here used with type 'a > > I guess that this is not a lambda term that can be typed. > There are many of them. A famous one is the Y combinator. > The _typed_ lambda calculus does not allow all the lambda terms > of the (normal) lambda calculus. g can't be written, but (f x) (x f) works for suitable values for f and x :) Namely if f = x = id. There's probably some deep parametricity property at the heart of it. marius