Re: Unexpected restriction in "let rec" expressions
 oleg@o...
[
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:  oleg@o... 
Subject:  Re: Unexpected restriction in "let rec" expressions 
Andrej Bauer wrote: > More precisely, consider any term > fix : (c > c) > c, > where the name "fix" suggests that we will plug in a fixpoint operator > at the end of the day. > ... > P.S. Can someone think of anything else other than a fixpoint operator > that we could use in place of fix to get an interesting program (maybe > for special cases of c, such as c = int > int)? `For special cases if c' makes the problem very easy. For example, let c = int: # let pseudofixint f : int = f 0;; val pseudofixint : (int > int) > int = <fun> or let c = int> int # let anotherpseudofix f : int > int = f (fun (x:int) > x);; val anotherpseudofix : ((int > int) > int > int) > int > int = <fun> It is only if we insist on a polymorphic function (for all c or at least c = a> b for all a and b) that we obtain that fix must be either a fixpoint combinator or a similar misbehaving term such as # let almostfix (f:'c > 'c) = f (failwith "what could you expect");; val almostfix : ('a > 'a) > 'a = <fun> This is because only fix or similar misbehaving combinators let us `produce' values that do not exist (or at least, claim to produce those values). For example: # type unicorn (* abstract *) # let f (x:unicorn) = x val f : unicorn > unicorn = <fun> Indeed, we can always demonstrate a value of the type c>c no matter how bizarre c is. Thus, expression (almostfix f) has the type unicorn and `gives' us the value of unicorns, `proving' that unicorns exist.