infinite types ? (haskell)
Lab. - konto DLIMP-17
Hello group.
I tried this function definition :
--fun :: Int -> a@[a]
fun n
| n>0 = [fun (n-1)]
| n==0 = []
| True = error "fun : arg is negative"
but when loaded into hugs (,my haskell interpreter at school,)
it showed this :
Reading file "inftypetst.hs":
Type checking
ERROR "inflist.hs" (line 3): Type error in function binding
*** term : fun
*** type : a -> [b]
*** does not match : a -> b
*** because : unification would give infinite type
so it seems that infinite types are disallowed in haskell ..
(or : no "loops" in type trees)
(if it would have worked, fun 2 would evaluate to [[[]]]::[[[a]]])
why ?
maybe it's hard to implement or typecheck or unify them ?
or do they make theorem proving harder ?
I'm not sure if one could come up with a legitimate problem which
could be solved with a function requiring infinite types and not nicely
solved without them..
(maybe church-numeral-functions,etc for lambda-calculus ?)
what do you think, are infinite types totally unneccesary ?
if one could implement them in haskell maybe somthing like a@[a] would be
a nice syntax for the type of a list of elements with the same type as the
whole list.
(feel free to correct me if I am talking rubbish, I just learned haskell
this spring)
------------------
Stefan Ljungstrand
Email : dlimp-17 and md9slj @mdstud.chalmers.se
URL : http://www.mdstud.chalmers.se/~dlimp-17/index.html
GM d- s: a--- C+(++) US P>+ L>+ E W++(+) N+ o? K- w O? M?(-)@ V? PS+() PE Y+
PGP?>+ t+ 5? X(+) R? tv(-) b+() DI(+) D? G e- h-- r? y
Michael Hudson
> Hello group.
>
> I tried this function definition :
>
> --fun :: Int -> a@[a]
> fun n
> | n>0 = [fun (n-1)]
> | n==0 = []
> | True = error "fun : arg is negative"
>
> but when loaded into hugs (,my haskell interpreter at school,)
> it showed this :
>
> Reading file "inftypetst.hs":
> Type checking
> ERROR "inflist.hs" (line 3): Type error in function binding
> *** term : fun
> *** type : a -> [b]
> *** does not match : a -> b
> *** because : unification would give infinite type
>
> so it seems that infinite types are disallowed in haskell ..
> (or : no "loops" in type trees)
>
> (if it would have worked, fun 2 would evaluate to [[[]]]::[[[a]]])
>
> why ?
I think the problem is that the type of the function result depends on
the runtime argument.
Infinite types are certainly possible, eg:
data Tree a = Leaf a | Node (Tree a) (Tree a)
You *might* be able to write your function "fun" using typeclasses of
some kind (but I'm not really sure).
HTH,
Michael
--
I really hope there's a catastrophic bug insome future e-mail
program where if you try and send an attachment it cancels your
ISP account, deletes your harddrive, and pisses in your coffee
-- Adam Rixey
Marcin 'Qrczak' Kowalczyk
> so it seems that infinite types are disallowed in haskell ..
> (or : no "loops" in type trees)
Yes, as long as you don't expand data and newtype definitions.
But you can have loops when they go through data or newtype:
newtype SelfList = SL [SelfList] deriving Show
fun :: Int -> SelfList
fun n
| n>0 = SL [fun (n-1)]
| n==0 = SL []
| True = error "fun : arg is negative"
Now, print (fun 5) prints SL [SL [SL [SL [SL [SL []]]]]].
> maybe it's hard to implement or typecheck or unify them ?
AFAIK yes, they make the type system undecidable.
--
__("< Marcin Kowalczyk * qrc...@knm.org.pl http://qrczak.ids.net.pl/
\__/ GCS/M d- s+:-- a23 C+++$ UL++>++++$ P+++ L++>++++$ E-
^^ W++ N+++ o? K? w(---) O? M- V? PS-- PE++ Y? PGP+ t
QRCZAK 5? X- R tv-- b+>++ DI D- G+ e>++++ h! r--%>++ y-
Francois Pottier
Lab. - konto DLIMP-17 <dlim...@mdstud.chalmers.se> wrote:
>maybe it's hard to implement or typecheck or unify them ?
Not particularly. Actually, it's even easier, because it only
amounts to removing the so-called `occur-check' from the
Hindley/Milner type inference engine.
The main reason why recursive types are not allowed is that, by
allowing them, many programs which are in fact erroneous would
become well-typed. (By erroneous, I don't mean that they would
crash; the system is still type-safe. I mean that they do not
behave as intended.) For example, look at the following code (in
O'Caml syntax):
let rec search predicate = function
| [] ->
raise Not_found
| hd :: tl ->
if predicate hd
then hd
else tl
A classic piece of code which looks for an element which satisfies
a given predicate within a given list. Only I forgot the recursive
call to: I wrote [tl] instead of [search predicate tl].
Without recursive types, O'Caml says:
This expression has type 'a list but is here used with type 'a
With recursive types (ocaml -rectypes), it says:
val search : (('a list as 'a) -> bool) -> 'a list -> 'a = <fun>
In other words, if arbitrary recursive types are allowed, then
the error is unnoticed by the compiler.
Of course, recursive data structures are useful; but we usually
require recursion to `go through' at list one data type constructor,
so occurrences of data constructors and `match' operations in the
code explicitly tell the compiler where to `fold/unfold' recursive
types.
Hope this helps,
Newsgroups: comp.lang.functional
Subject: Re: infinite types ? (haskell)
Summary:
Expires:
References: <Pine.SOL.4.21.00052...@scooter.mdstud.chalmers.se>
Sender:
Followup-To:
Distribution:
Organization:
Keywords:
Cc: dlim...@mdstud.chalmers.se,Francois...@inria.fr
In article <Pine.SOL.4.21.00052...@scooter.mdstud.chalmers.se>,
Lab. - konto DLIMP-17 <dlim...@mdstud.chalmers.se> wrote:
>maybe it's hard to implement or typecheck or unify them ?
Not particularly. Actually, it's even easier, because it only
amounts to removing the so-called `occur-check' from the
Hindley/Milner type inference engine.
The main reason why recursive types are not allowed is that, by
allowing them, many programs which are in fact erroneous would
become well-typed. (By erroneous, I don't mean that they would
crash; the system is still type-safe. I mean that they do not
behave as intended.) For example, look at the following code (in
O'Caml syntax):
let rec search predicate = function
| [] ->
raise Not_found
| hd :: tl ->
if predicate hd
then hd
else tl
A classic piece of code which looks for an element which satisfies
a given predicate within a given list. Only I forgot the recursive
call to: I wrote [tl] instead of [search predicate tl].
Without recursive types, O'Caml says:
This expression has type 'a list but is here used with type 'a
With recursive types (ocaml -rectypes), it says:
val search : (('a list as 'a) -> bool) -> 'a list -> 'a = <fun>
In other words, if arbitrary recursive types are allowed, then
the error is unnoticed by the compiler.
Of course, recursive data structures are useful; but we usually
require recursion to `go through' at list one data type constructor,
so occurrences of data constructors and `match' operations in the
code explicitly tell the compiler where to `fold/unfold' recursive
types.
Hope this helps,
Newsgroups: comp.lang.functional
Subject: Re: infinite types ? (haskell)
Summary:
Expires:
References: <Pine.SOL.4.21.00052...@scooter.mdstud.chalmers.se>
Sender:
Followup-To:
Distribution:
Organization: INRIA Rocquencourt, BP 105, 78153 Le Chesnay Cedex, France
Keywords:
Cc: dlim...@mdstud.chalmers.se,Francois...@inria.fr
In article <Pine.SOL.4.21.00052...@scooter.mdstud.chalmers.se>,
Lab. - konto DLIMP-17 <dlim...@mdstud.chalmers.se> wrote:
>maybe it's hard to implement or typecheck or unify them ?
Not particularly. Actually, it's even easier, because it only
amounts to removing the so-called `occur-check' from the
Hindley/Milner type inference engine.
The main reason why recursive types are not allowed is that, by
allowing them, many programs which are in fact erroneous would
become well-typed. (By erroneous, I don't mean that they would
crash; the system is still type-safe. I mean that they do not
behave as intended.) For example, look at the following code (in
O'Caml syntax):
let rec search predicate = function
| [] ->
raise Not_found
| hd :: tl ->
if predicate hd
then hd
else tl
A classic piece of code which looks for an element which satisfies
a given predicate within a given list. Only I forgot the recursive
call to: I wrote [tl] instead of [search predicate tl].
Without recursive types, O'Caml says:
This expression has type 'a list but is here used with type 'a
With recursive types (ocaml -rectypes), it says:
val search : (('a list as 'a) -> bool) -> 'a list -> 'a = <fun>
In other words, if arbitrary recursive types are allowed, then
the error is unnoticed by the compiler.
Of course, recursive data structures are useful; but we usually
require recursion to `go through' at list one data type constructor,
so occurrences of data constructors and `match' operations in the
code explicitly tell the compiler where to `fold/unfold' recursive
types.
Hope this helps,
Newsgroups: comp.lang.functional
Subject: Re: infinite types ? (haskell)
Summary:
Expires:
References: <Pine.SOL.4.21.00052...@scooter.mdstud.chalmers.se>
Sender:
Followup-To:
Distribution:
Organization:
Keywords:
Cc: dlim...@mdstud.chalmers.se,Francois...@inria.fr
In article <Pine.SOL.4.21.00052...@scooter.mdstud.chalmers.se>,
Lab. - konto DLIMP-17 <dlim...@mdstud.chalmers.se> wrote:
>maybe it's hard to implement or typecheck or unify them ?
Not particularly. Actually, it's even easier, because it only
amounts to removing the so-called `occur-check' from the
Hindley/Milner type inference engine.
The main reason why recursive types are not allowed is that, by
allowing them, many programs which are in fact erroneous would
become well-typed. (By erroneous, I don't mean that they would
crash; the system is still type-safe. I mean that they do not
behave as intended.) For example, look at the following code (in
O'Caml syntax):
let rec search predicate = function
| [] ->
raise Not_found
| hd :: tl ->
if predicate hd
then hd
else tl
A classic piece of code which looks for an element which satisfies
a given predicate within a given list. Only I forgot the recursive
call to: I wrote [tl] instead of [search predicate tl].
Without recursive types, O'Caml says:
This expression has type 'a list but is here used with type 'a
With recursive types (ocaml -rectypes), it says:
val search : (('a list as 'a) -> bool) -> 'a list -> 'a = <fun>
In other words, if arbitrary recursive types are allowed, then
the error is unnoticed by the compiler.
Of course, recursive data structures are useful; but we usually
require recursion to `go through' at list one data type constructor,
so occurrences of data constructors and `match' operations in the
code explicitly tell the compiler where to `fold/unfold' recursive
types.
Hope this helps,
--
François Pottier
Francois...@inria.fr
http://pauillac.inria.fr/~fpottier/
Andreas Rossberg
>
> so it seems that infinite types are disallowed in haskell ..
> (or : no "loops" in type trees)
Yes, such recursive types are not directly allowed in Haskell - you have
to wrap them up into a data type.
> why ?
>
> maybe it's hard to implement or typecheck or unify them ?
It's not much harder. There are/were languages that have general
recursive types (eg. Hope?). However, it turns out that in practice they
are not very useful. In languages with type inference they just
obfuscate errors in your code most of the times: you write some complex
function, get it wrong, but the type checker does not complain but just
deduces an obscure recursive type. At the point of application you get
strange and hard to decode error messages.
I believe some early versions of OCaml also allowed arbitrary recursive
types, but they have been restricted to object types later because users
complained.
> what do you think, are infinite types totally unneccesary ?
No, but that's one reason for having datatypes. They essentially give
you the same expressiveness, though slightly more cumbersome. In Haskell
you can also use newtype.
--
Andreas Rossberg, ross...@ps.uni-sb.de
:: be declarative. be functional. just be. ::
Lab. - konto DLIMP-17
> I believe some early versions of OCaml also allowed arbitrary recursive
> types, but they have been restricted to object types later because users
> complained.
Maybe recursive types could be allowed only when you specifically ask for
them with some syntax, and otherwise not allowed .. ?
>
> > what do you think, are infinite types totally unneccesary ?
>
> No, but that's one reason for having datatypes. They essentially give
> you the same expressiveness, though slightly more cumbersome. In Haskell
> you can also use newtype.
One resaon for asking about this is :
I recently read about and became very interested in lambda calculus and
combinator graph reduction.
So I try to make a small (untyped right now) Lambda interpreter in
haskell (and SKI reduction engine in C ..)
(with data LExpr = Var String | App LExpr LExpr | Lam String Lexpr
... and so on)
I saw some sort of list representing in lambda calculus where
a list was a pair of it's car and cdr (head and tail).
But I thought of a more interesting one :
(sort of extrapolating church numerals)
let nil = \c.\z.z
let cons = \x.\xs.\c.\z.c x (xs c z)
let isnil = \xs.xs (\_.\_.false) true
let car = \xs.xs true (error car_nil)
let cdr = \xs.snd (xs (\y.\ys.pair (cons y (fst y))
(fst y) )
(pair nil (error cdr_nil)) )
let length = \xs.xs (\_.succ) zero
let append = \xs.\ys.xs cons ys
where true,false,pair,fst,snd,zero,succ has usual definitions
append is interestingly short here
cdr is a paralell to pred, thusly more expensive than a cdr based on a
pair-list (which would just be snd)
Now i tried to translate these definitions directly to haskell functions !
the booleans,numerals and lists seem to work
(I can even define a type for numerals : (a -> a) -> a -> a , but not for
booleans)
but twice (\x.x x) and yfix (\f.twice (\x.f (x x))) don't work (at least
directly) because of no infinite types...
So, can twice and yfix be modelled directly as haskell functions ?
Frank Meisschaert
: Hello group.
: I tried this function definition :
: --fun :: Int -> a@[a]
: fun n
: | n>0 = [fun (n-1)]
: | n==0 = []
: | True = error "fun : arg is negative"
: but when loaded into hugs (,my haskell interpreter at school,)
: it showed this :
: Reading file "inftypetst.hs":
: Type checking
: ERROR "inflist.hs" (line 3): Type error in function binding
: *** term : fun
: *** type : a -> [b]
: *** does not match : a -> b
: *** because : unification would give infinite type
: so it seems that infinite types are disallowed in haskell ..
: (or : no "loops" in type trees)
not really, recursive types are allowed, and they are mostly infinite.
: (if it would have worked, fun 2 would evaluate to [[[]]]::[[[a]]])
: why ?
there is a conflict in types: fun is defined as returning a list while from
inference it follows that it returns an arbitrary type. If you would try to
unify that, the type results as
fun :: Int -> [] [] [] [] [] [] ... (a)
an infinite intersection of lists. I put the a between parentheses since it
is NEVER reached.
: maybe it's hard to implement or typecheck or unify them ?
: or do they make theorem proving harder ?
a theorem prover works in essence on the language in which the theorem is
stated.
: I'm not sure if one could come up with a legitimate problem which
: could be solved with a function requiring infinite types and not nicely
: solved without them..
: (maybe church-numeral-functions,etc for lambda-calculus ?)
Your true infinite types seem a lot like sets with an uncountable amount of
elements. These are impossible to use in any programming language.
: what do you think, are infinite types totally unneccesary ?
: if one could implement them in haskell maybe somthing like a@[a] would be
: a nice syntax for the type of a list of elements with the same type as the
: whole list.
Russels paradox, remember?
: (feel free to correct me if I am talking rubbish, I just learned haskell
: this spring)
: ------------------
Vincent Zweije
<ross...@ps.uni-sb.de> wrote:
|| "Lab. - konto DLIMP-17" wrote:
|| >
|| > so it seems that infinite types are disallowed in haskell ..
|| > maybe it's hard to implement or typecheck or unify them ?
||
|| It's not much harder. There are/were languages that have general
|| recursive types (eg. Hope?). However, it turns out that in practice they
|| are not very useful. In languages with type inference they just
|| obfuscate errors in your code most of the times: you write some complex
|| function, get it wrong, but the type checker does not complain but just
|| deduces an obscure recursive type. At the point of application you get
|| strange and hard to decode error messages.
That is more a problem of type inference versus type checking.
The compiler infers a more specific type (recursive) than the one you
intended. It can happen just the same with non-recursive types. You get
an obscure typing error at a seemingly unrelated place in your program.
Specify the type when you write a function. It's the only way to be
sure a type error in your function definition doesn't progress to another
place in the program.
|| I believe some early versions of OCaml also allowed arbitrary recursive
|| types, but they have been restricted to object types later because users
|| complained.
Maybe their minds weren't geared to think about recursive types (yet)?
Ciao. Vincent.
--
Vincent Zweije <zwe...@xs4all.nl> | "If you're flamed in a group you
<http://www.xs4all.nl/~zweije/> | don't read, does anybody get burnt?"
[Xhost should be taken out and shot] | -- Paul Tomblin on a.s.r.
Fergus Henderson
>Lab. - konto DLIMP-17 (dlim...@mdstud.chalmers.se) wrote:
>
>: I tried this function definition :
>
>: --fun :: Int -> a@[a]
>: fun n
>: | n>0 = [fun (n-1)]
>: | n==0 = []
>: | True = error "fun : arg is negative"
>
>: but when loaded into hugs [...] it showed this :
>
>: ERROR "inflist.hs" (line 3): Type error in function binding [...]
>: *** because : unification would give infinite type
>
>: so it seems that infinite types are disallowed in haskell ..
>: (or : no "loops" in type trees)
>
>not really, recursive types are allowed, and they are mostly infinite.
No, infinite types are disallowed in Haskell. Recursive types are
allowed, but recursive types are finite types, not infinite types.
Data values whose type is recursive can be infinite, but the types
themselves are finite.
>: maybe it's hard to implement or typecheck or unify them ?
I think it does complicate the implementation a little, but not too
much. On the other hand, they are not very useful; they're not needed
often, and for those few times when you might need an infinite type,
you can always modify your program a little so that it uses a
recursive newtype instead.
>: I'm not sure if one could come up with a legitimate problem which
>: could be solved with a function requiring infinite types and not nicely
>: solved without them..
>: (maybe church-numeral-functions,etc for lambda-calculus ?)
>Your true infinite types seem a lot like sets with an uncountable amount of
>elements. These are impossible to use in any programming language.
I don't agree. Of course any language which supports infinite types
can't support *all* possible infinite types, but you can fairly easily
support the subset which have a finite cyclic representation. This is just
like the way languages such as Haskell which support infinite data
values don't allow *all* possible infinite data values, but do support
those infinite data values which have a finite cyclic representation.
--
Fergus Henderson <f...@cs.mu.oz.au> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger f...@128.250.37.3 | -- the last words of T. S. Garp.
Andreas Rossberg
>
> || It's not much harder. There are/were languages that have general
> || recursive types (eg. Hope?). However, it turns out that in practice they
> || are not very useful. In languages with type inference they just
> || obfuscate errors in your code most of the times: you write some complex
> || function, get it wrong, but the type checker does not complain but just
> || deduces an obscure recursive type. At the point of application you get
> || strange and hard to decode error messages.
>
> That is more a problem of type inference versus type checking.
True, but the question was about Haskell and Haskell is a language with
type inference. This feature tends to become a lot less useful in the
presence of general recursive types and many users wouldn't like that, I
believe.
Of course, when you don't care about type inference than you don't have
to mind at all. Personally, I prefer to have the luxury of type
inference. But please, no flame war about type inference.
Actually the way the trade-off has been taken in Haskell, ML, and
similar languages is not far from what you want. The general idea is
that any typing feature that is more or less incompatible with type
inference (recursive types, higher-order quantification, etc.) can only
be used in conjunction with an explicit datatype. The use of a
datatype's constructor is sort of an implicit type annotation. This way,
you can add almost anything to the type system without compromising type
inference for everyday's work. And the overhead for using some of the
more exotic features is not much higher than in a language without type
inference.
> The compiler infers a more specific type (recursive) than the one you
> intended.
No, the point was about the compiler infering a type for something that
actually was a mistake on the user's side. We want to get as much help
from the compiler and the type system as we can in finding different
classes of errors, don't we? In by far most of the cases when a
recursive type is infered it is probably not what you intended.
> It can happen just the same with non-recursive types. You get
> an obscure typing error at a seemingly unrelated place in your program.
Yes, but not that often and not that obscure, IMO.
> || I believe some early versions of OCaml also allowed arbitrary recursive
> || types, but they have been restricted to object types later because users
> || complained.
>
> Maybe their minds weren't geared to think about recursive types (yet)?
The OCaml team has a lot of expertise in types, particularly in
recursive types (just look at the object system). And they sure know a
lot about the practical side of type systems.
Jerzy Karczmarczuk
> : I'm not sure if one could come up with a legitimate problem which
> : could be solved with a function requiring infinite types and not nicely
> : solved without them..
> : (maybe church-numeral-functions,etc for lambda-calculus ?)
> Your true infinite types seem a lot like sets with an uncountable
> amount of elements. These are impossible to use in any programming
> language.
1. Church numerals are quite easy to define in Haskell, I never
needed infinite types. Am I missing some Horrible Truth?
2. What do you mean that it is impossible to use sets with uncountable
number of elements?
That we cannot use reals, complexes, functional objects?
Well, if you are a Jesuit you will say that we use only finite
discrete approximations of everything, <<y compris>> the
functional objects, but sincerely, I don't care at at whether
they are countable.
Jerzy Karczmarczuk
Caen, France
Edward Avis
>2. What do you mean that it is impossible to use sets with uncountable
> number of elements?
Suppose that in some language (eg Haskell) you could have types that
have an uncountable number of elements. Then just list all strings of
zero, one, two... characters and throw away those which aren't valid
Haskell or don't parse as an element of this type. You are left with
a list of all elements of this type, or rather any element will be
reached in the end, so it is countable after all! (does that make
sense people?)
> That we cannot use reals, complexes, functional objects?
Yep, you cannot have reals. Only rational numbers or some other
countable set like nth roots of rational numbers. Whatever you pick
would not include all real numbers.
As for functional objects, you can have only _computable_ functions,
and they are countable, I think.
--
Ed Avis
ep...@doc.ic.ac.uk
Fergus Henderson
>Jerzy Karczmarczuk <kar...@info.unicaen.fr> writes:
>
>>2. What do you mean that it is impossible to use sets with uncountable
>> number of elements?
>
>Suppose that in some language (eg Haskell) you could have types that
>have an uncountable number of elements. Then just list all strings of
>zero, one, two... characters and throw away those which aren't valid
>Haskell or don't parse as an element of this type. You are left with
>a list of all elements of this type, or rather any element will be
>reached in the end, so it is countable after all! (does that make
>sense people?)
That proof is flawed, because it makes some additional unstated
assumptions. By "You are left with a list of all elements of this type",
do you mean that the list contains only elements of this type (true),
or that the list necessarily contains all the elements of this
type? The latter doesn't follow from your construction.
You're assuming that every element of the type can be expressed in a
piece of code that parses as an element of the type, and that
each such piece of code corresponds with exactly one element of the
type. But that need not be the case, and indeed it is not the case in
Haskell.
For example, in the following program
import Random
main = do g <- getStdGen
let r = randoms g
print (r :: [Bool])
the set of values which `r' can take is uncountable.
>> That we cannot use reals, complexes, functional objects?
>
>Yep, you cannot have reals. Only rational numbers or some other
>countable set like nth roots of rational numbers. Whatever you pick
>would not include all real numbers.
If you interpret the list of booleans output by the above program as
binary digits after the decimal point (or should I say binary point?),
then the possible outputs of that program include all real numbers in
the range (0,1). Modifying this to print the output in a more conventional
notation or extend the range all real numbers are left as simple exercises
for the reader.
Nick Williams
Edward Avis <ep...@doc.ic.ac.uk> wrote:
>As for functional objects, you can have only _computable_ functions,
>and they are countable, I think.
Yes; given that there are only a countably infinite number of
transitions possible in a Turing machine, the number of Turing
computable functions is at most countably finite. But, it is
also at least countably infinite, since there are countably many
constant functions, all of which are Turing computable.
Cheers,
Nick.
--
[ Nick Williams ]
[ MSc Computation Mobile - 07957-138179 ]
[ New College, Oxford http://www.new.ox.ac.uk/~nick/ ]
Daniel C. Wang
f...@cs.mu.oz.au (Fergus Henderson) writes:
{stuff deleted}
> No, infinite types are disallowed in Haskell. Recursive types are
> allowed, but recursive types are finite types, not infinite types.
> Data values whose type is recursive can be infinite, but the types
> themselves are finite.
I don't buy this distinction between infinite and recursive. A recursive
type is just finite notation for a type tree of infinite size. Just as
(a|b)* is a finite representation of an infinite regular set.
Edward Avis
>>Suppose that in some language (eg Haskell) you could have types that
>>have an uncountable number of elements. Then just list all strings of
>>zero, one, two... characters and throw away those which aren't valid
>>Haskell or don't parse as an element of this type. You are left with
>>a list of all elements of this type, or rather any element will be
>>reached in the end, so it is countable after all! (does that make
>>sense people?)
>
>That proof is flawed, because it makes some additional unstated
>assumptions. By "You are left with a list of all elements of this type",
>do you mean that the list contains only elements of this type (true),
>or that the list necessarily contains all the elements of this
>type?
I assumed both, thinking that any datatype in Haskell is defined with
one or more constructors. Pick a constructor and then list all possible
elements for each of the constructor's arguments. Do this for all the
possible constructors (in a depth-first manner) and you will eventually
list all the elements of the type.
Note that this doesn't include 'infinite' elements such as an infinitely
long list. Such a value never actually exists during evaluation of a
Haskell program, it's just a device to help people reason about
programs. There is no bound on the length of lists, but any list you do
manage to compute fully will be finite.
>For example, in the following program
>
> import Random
> main = do g <- getStdGen
> let r = randoms g
> print (r :: [Bool])
>
>the set of values which `r' can take is uncountable.
Surely r can take the following values at various stages during the
computation:
_|_
False : _|_
True : _|_
False : False : _|_
False : True : _|_
True : False : _|_
True : True : _|_
and so on, which is countable. It's uncountable only if you ignore the
fact that r is never fully computed.
Also I think there may be another problem with the example you
give. For any value of g there is only _one_ possible value of
(randoms g). Putting the thing inside the IO monad means that which
particular g you get depends on the outside world, but for any given
state of the world, there is only one possible value of r.
Would it be possible to give an example which is not in the IO monad?
>If you interpret the list of booleans output by the above program as
>binary digits after the decimal point (or should I say binary point?),
>then the possible outputs of that program include all real numbers in
>the range (0,1).
I don't think so. There are two cases: I interrupt the program while it
is running, and I don't interrupt it.
- If I interrupt the program during its run, the output so far is a
rational number.
- If I do not interrupt the program, it never terminates and thus does
not produce a result at all.
No matter how long you left the program running for, it could never
produce the value of pi.
--
Ed Avis
ep...@doc.ic.ac.uk
Fergus Henderson
>On 29 May 2000, Fergus Henderson wrote:
>
>>For example, in the following program
>>
>> import Random
>> main = do g <- getStdGen
>> let r = randoms g
>> print (r :: [Bool])
>>
>>the set of values which `r' can take is uncountable.
>
>Surely r can take the following values at various stages during the
>computation:
>
>_|_
>
>False : _|_
>True : _|_
>
>False : False : _|_
>False : True : _|_
>True : False : _|_
>True : True : _|_
>
>and so on,
No. `r' never takes the value `_|_', or `False : _|_', etc.
If `r' took the value `_|_', then the program would either
loop infinitely without producing any output, or would abort
with an error message. But the program does not do that.
I think you misunderstand the meaning of `_|_'.
It does not mean an unevaluated closure.
Also I think you missed the distinction between value and
representation. If we use `<closure>' to denote an unevaluated
closure, then at different points in the computation, `r' may have the
representations
<closure>
False : <closure>
True : <closure>
and so on, but the representation of `r' is not the same as its value.
The representation at any given point in time is finite, but the value
is infinite.
>Also I think there may be another problem with the example you
>give. For any value of g there is only _one_ possible value of
>(randoms g). Putting the thing inside the IO monad means that which
>particular g you get depends on the outside world, but for any given
>state of the world, there is only one possible value of r.
That's true, but I don't see why it is a "problem".
>Would it be possible to give an example which is not in the IO monad?
The IO monad is a standard part of Haskell, and indeed it is not
possible to write a Haskell program without using it.
So I consider it fair game ;-)
>>If you interpret the list of booleans output by the above program as
>>binary digits after the decimal point (or should I say binary point?),
>>then the possible outputs of that program include all real numbers in
>>the range (0,1).
>
>I don't think so. There are two cases: I interrupt the program while it
>is running, and I don't interrupt it.
>
>- If I interrupt the program during its run, the output so far is a
>rational number.
OK.
>- If I do not interrupt the program, it never terminates
OK...
>and thus does not produce a result at all.
Here I disagree. If you were to say instead that it doesn't
ever produce a _complete_ result, I'd agree.
>No matter how long you left the program running for, it could never
>produce the value of pi.
Certainly it could never produce the value of pi, since that is not in
the range (0,1) ;-) And it could never _completely_ produce the value
of pi/4. But with the right random number generator and the right
seed, it could indeed be the case that this program generates pi/4, in
the sense that it keeps outputting digits and its output at any given
point in time is always a correct prefix of the binary digits of pi/4.
In such a case, I think it is fair to say that "the output of the
program is pi/4", even though the binary expansion of pi/4 is infinitely
long and thus cannot be completely output in any finite time.
P.S.
With a truly random random number generator, the chance of generating
pi/4 would be zero. But Haskell does not require the random number
generator in its standard library to be truly random.
Edward Avis
>given that there are only a countably infinite number of
>transitions possible in a Turing machine, the number of Turing
>computable functions is at most countably finite.
You mean countably infinite, right?
>But, it is
>also at least countably infinite, since there are countably many
>constant functions, all of which are Turing computable.
There are uncountably many constant functions. Eg there is one
constant function for each real number.
There is a countably infinite number of constant functions returning
an integer (for example), each of which is Turing computable.
--
Ed Avis
ep...@doc.ic.ac.uk
Vincent Zweije
<f...@cs.mu.oz.au> wrote:
|| Edward Avis <ep...@doc.ic.ac.uk> writes:
||
|| >Jerzy Karczmarczuk <kar...@info.unicaen.fr> writes:
|| >
|| >>2. What do you mean that it is impossible to use sets with uncountable
|| >> number of elements?
|| >
|| >Suppose that in some language (eg Haskell) you could have types that
|| >have an uncountable number of elements. Then just list all strings of
|| >zero, one, two... characters and throw away those which aren't valid
|| >Haskell or don't parse as an element of this type. You are left with
|| >a list of all elements of this type, or rather any element will be
|| >reached in the end, so it is countable after all! (does that make
|| >sense people?)
||
|| That proof is flawed, because it makes some additional unstated
|| assumptions.
Are you attacking the proof or the conclusion?
|| By "You are left with a list of all elements of this type",
|| do you mean that the list contains only elements of this type (true),
|| or that the list necessarily contains all the elements of this
|| type? The latter doesn't follow from your construction.
|| You're assuming that every element of the type can be expressed in a
|| piece of code that parses as an element of the type, and that
|| each such piece of code corresponds with exactly one element of the
|| type. But that need not be the case, and indeed it is not the case in
|| Haskell.
||
|| For example, in the following program
||
|| import Random
|| main = do g <- getStdGen
|| let r = randoms g
|| print (r :: [Bool])
||
|| the set of values which `r' can take is uncountable.
Haskell (or any other) programs are finite. Any value you specify with
it is from a countably infinite type at the most.
If you depend on some form of IO, the specification you have given is
not complete; you still need to know what input you give it to know the
output value. Rather, you must say that you have specified a function
from the input to the output.
You could have language primitives with an uncountably infinite type.
However, I'd like to see an implementation provide these first.
And anyway, you could see language primitives as just another form of IO.
Vincent Zweije
<ross...@ps.uni-sb.de> wrote:
|| Vincent Zweije wrote:
|| >
|| > || It's not much harder. There are/were languages that have general
|| > || recursive types (eg. Hope?). However, it turns out that in practice
|| > || they are not very useful. In languages with type inference they just
|| > || obfuscate errors in your code most of the times: you write some
|| > || complex function, get it wrong, but the type checker does not
|| > || complain but just deduces an obscure recursive type. At the point of
|| > || application you get strange and hard to decode error messages.
|| >
|| > That is more a problem of type inference versus type checking.
||
|| True, but the question was about Haskell and Haskell is a language with
|| type inference. This feature tends to become a lot less useful in the
|| presence of general recursive types and many users wouldn't like that, I
|| believe.
In my opinion, a language should be a programming tool, not a policy.
You provide a means of writing programs, but you do not specify how they
are used; you leave its usage to the programmer.
That being said, I can see that a feature (recursive types) that allows
significantly more bad programs to pass than that it adds to ease of
programming is probably not a good thing.
Then again, the programmer can always specify the function types, and
prevent abscure type error messages by confining them to the function
with the error. Personally, the first thing I do with a type error is
to specify the type of more or less every function in sight, and then go
from there; I use inference very sparingly (one liner functions mostly).
|| Of course, when you don't care about type inference than you don't have
|| to mind at all. Personally, I prefer to have the luxury of type
|| inference. But please, no flame war about type inference.
||
|| Actually the way the trade-off has been taken in Haskell, ML, and
|| similar languages is not far from what you want. The general idea is
|| that any typing feature that is more or less incompatible with type
|| inference (recursive types, higher-order quantification, etc.) can only
|| be used in conjunction with an explicit datatype. The use of a
|| datatype's constructor is sort of an implicit type annotation. This way,
|| you can add almost anything to the type system without compromising type
|| inference for everyday's work. And the overhead for using some of the
|| more exotic features is not much higher than in a language without type
|| inference.
This does sound like a good trade-off, provided that recursive types
really produce such more obscure type errors than non-recursive ones.
I'm not really sure about that (having no real experience) but I'll take
your word for it.
|| > The compiler infers a more specific type (recursive) than the one you
|| > intended.
||
|| No, the point was about the compiler infering a type for something that
|| actually was a mistake on the user's side. We want to get as much help
|| from the compiler and the type system as we can in finding different
|| classes of errors, don't we? In by far most of the cases when a
|| recursive type is infered it is probably not what you intended.
I agree with your point. However, in my experience, a programming
mistake usually leads to a type error *somewhere*. That's enough;
after that you can specify types of functions to find out the source of
the problem.
|| > It can happen just the same with non-recursive types. You get
|| > an obscure typing error at a seemingly unrelated place in your program.
||
|| Yes, but not that often and not that obscure, IMO.
When you get into third or higher order functions (f::(((a->b)->c)->d))
and enough type aliases, every type error is obscure. In a few cases I
have had to copy & paste my unification error messages and format them
just to find the difference between the two types that wouldn't unify.
And only then start to find out which programming mistake I made (Can
you tell I rely on type checking? :-).
|| > || I believe some early versions of OCaml also allowed arbitrary
|| > || recursive types, but they have been restricted to object types later
|| > || because users complained.
|| >
|| > Maybe their minds weren't geared to think about recursive types (yet)?
||
|| The OCaml team has a lot of expertise in types, particularly in
|| recursive types (just look at the object system). And they sure know a
|| lot about the practical side of type systems.
I am sure the OCaml team know what they're doing, but I was thinking the
"users" you mentioned would be using OCaml, not developing it.
Fergus Henderson
>Fergus Henderson <f...@cs.mu.oz.au> wrote:
>
>|| Edward Avis <ep...@doc.ic.ac.uk> writes:
>||
>|| >Jerzy Karczmarczuk <kar...@info.unicaen.fr> writes:
>|| >
>|| >>2. What do you mean that it is impossible to use sets with uncountable
>|| >> number of elements?
>|| >
>|| >Suppose that in some language (eg Haskell) you could have types that
>|| >have an uncountable number of elements. Then just list all strings of
>|| >zero, one, two... characters and throw away those which aren't valid
>|| >Haskell or don't parse as an element of this type. You are left with
>|| >a list of all elements of this type, or rather any element will be
>|| >reached in the end, so it is countable after all! (does that make
>|| >sense people?)
>||
>|| That proof is flawed, because it makes some additional unstated
>|| assumptions.
>
>Are you attacking the proof or the conclusion?
Both.
>|| By "You are left with a list of all elements of this type",
>|| do you mean that the list contains only elements of this type (true),
>|| or that the list necessarily contains all the elements of this
>|| type? The latter doesn't follow from your construction.
>|| You're assuming that every element of the type can be expressed in a
>|| piece of code that parses as an element of the type, and that
>|| each such piece of code corresponds with exactly one element of the
>|| type. But that need not be the case, and indeed it is not the case in
>|| Haskell.
>||
>|| For example, in the following program
>||
>|| import Random
>|| main = do g <- getStdGen
>|| let r = randoms g
>|| print (r :: [Bool])
>||
>|| the set of values which `r' can take is uncountable.
>
>Haskell (or any other) programs are finite. Any value you specify with
>it is from a countably infinite type at the most.
That's true. But in the above program, the value that `r' will take
is deliberately not specified -- `r' is supposed to be random.
So although it's true that any value which you can completely specify
with Haskell must come from a countabe set, it's not true that all
values which can be *used* in Haskell programs must come from a
countable set.
>You could have language primitives with an uncountably infinite type.
Indeed, Haskell does -- see the example above.
(To be precise, we should be talking about a type with an uncountably
infinite set of values, not an uncountably infinite type.)
Matthias Blume
> That's true. But in the above program, the value that `r' will take
> is deliberately not specified -- `r' is supposed to be random.
> So although it's true that any value which you can completely specify
> with Haskell must come from a countabe set, it's not true that all
> values which can be *used* in Haskell programs must come from a
> countable set.
Of course, since every countable set can be embedded into a larger
uncountable set, every value that a program might specify or use can
be seen as a member of such an uncountable set. But whenever you do
so and view a type as a set of uncountably many elements, you
_necessarily_ consider elements that never matter to any program using
this type.
In your example, any program that "uses" r will not be able to
actually see all of it. In other words, the observable behavior of
such a program always depends on no more than a countable
approximation of r.
As a matter of fact, your "r", when seen as a real number, is not
really a value because it will never be fully realized. Instead, this
"r" is a computation that, given time, can produce any one of the many
finite (and hence countable) approximations of that real number. As a
result, your program never "uses" anything that must be considered
part of an uncountable set.
Matthias
--
Matthias Blume <blume@k_u_r_i_m_s.k_y_o_t_o-u.a_c.j_p>
Kyoto University, Research Institute for Mathematical Sciences
(remove those spam-preventing underscores from mail address)
Edward Avis
>So although it's true that any value which you can completely specify
>with Haskell must come from a countabe set, it's not true that all
>values which can be *used* in Haskell programs must come from a
>countable set.
It depends what you mean by 'used'.
I would say: any value you use in a Haskell program must take a finite
amount of memory. Otherwise the program would never terminate (any
terminating TM uses a finite amount of space). All the possible
bit-patterns fitting in a finite amount of memory are countable. Thus
the values you can use in a Haskell program are countable.
--
Ed Avis
ep...@doc.ic.ac.uk
Edward Avis
>>>For example, in the following program
>>>
>>> import Random
>>> main = do g <- getStdGen
>>> let r = randoms g
>>> print (r :: [Bool])
>>>
>>>the set of values which `r' can take is uncountable.
>I think you misunderstand the meaning of `_|_'.
>It does not mean an unevaluated closure.
Oops. Sorry 'bout that.
>Also I think you missed the distinction between value and
>representation. If we use `<closure>' to denote an unevaluated
>closure, then at different points in the computation, `r' may have the
>representations
>
> <closure>
>
> False : <closure>
> True : <closure>
>
>and so on, but the representation of `r' is not the same as its value.
>The representation at any given point in time is finite, but the value
>is infinite.
I think I get it now. But if we are doing Haskell _programming_,
rather than just using Haskell as a way of representing functions,
then it is only the representations which are important. You can't
input or output any value unless you can find a representation for
it. And you can't fully compute it either.
>>For any value of g there is only _one_ possible value of
>>(randoms g). Putting the thing inside the IO monad means that which
>>particular g you get depends on the outside world, but for any given
>>state of the world, there is only one possible value of r.
>
>That's true, but I don't see why it is a "problem".
IIRC the original statement was that the range of values r can take is
uncountable. But it seems to me that the above code isn't really
giving r a value at all, but rather specifying a mapping between
state-of-the-world and value. I dunno, it just seems like cheating to
me...
>>- If I do not interrupt the program, it never terminates
>
>OK...
>
>>and thus does not produce a result at all.
>
>Here I disagree. If you were to say instead that it doesn't
>ever produce a _complete_ result, I'd agree.
Okay, we'll go with what you say, that it produces a _partial_ result.
This partial result must be a finite list. The finite lists of Bool
are countable.
>Certainly it could never produce the value of pi, since that is not in
>the range (0,1) ;-) And it could never _completely_ produce the value
>of pi/4. But with the right random number generator and the right
>seed, it could indeed be the case that this program generates pi/4, in
>the sense that it keeps outputting digits and its output at any given
>point in time is always a correct prefix of the binary digits of
>pi/4.
I'd say it 'approximates' pi/4. In an abstract sense, yes, it could
generate an irrational number, but for a Haskell _program_ which has
to run on a real computer with limited time and space, this isn't
possible.
I think that distinguishing between values and representations has
probably cleared up the confusion?
--
Ed Avis
ep...@doc.ic.ac.uk
Fergus Henderson
>f...@cs.mu.oz.au (Fergus Henderson) writes:
>{stuff deleted}
>> No, infinite types are disallowed in Haskell. Recursive types are
>> allowed, but recursive types are finite types, not infinite types.
>> Data values whose type is recursive can be infinite, but the types
>> themselves are finite.
>
>I don't buy this distinction between infinite and recursive.
Well, there's certainly an important conceptual difference between
recursive algebraic (discriminated union) types like
data Foo = F [Foo] -- Haskell syntax
and recursive type synonyms like
type Baz = [Baz] -- (illegal) Haskell syntax
Many languages, such as Haskell, Mercury, etc., treat these two
categories differently, allowing types in the first category but
not allowing types in the second category. So we need different
terms for these two kinds of types.
If you don't like the terms `infinite' and `recursive',
what terms would you suggest?
I guess we could talk about recursive algebraic types v.s.
recursive type synonyms. But there is an important sense
in which recursive type synonyms are infinite whereas
recursive algebraic types are not -- see below.
>A recursive type is just finite notation for a type tree of infinite size.
I don't agree. Mercury, Haskell and most other functional languages
use name equivalence rather than structural equivalence for
user-defined algebraic types. If in Mercury I write
:- type foo ---> f(list(foo)). % This Mercury syntax
% means the same as the
% Haskell example above
:- type bar ---> f(list(bar)).
then the infinite type trees that you would get by unrolling the
definitions for `foo' and `bar' would be the same:
`f(list(f(list(f(list(...))))))'. But because the language uses name
equivalence rather than structural equivalence, the two types are
distinct. This shows that you can't just treat a recursive type as
equivalent to its infinite unrolling.
In contrast, for type synonyms, like `Baz' in the earlier example,
Haskell and Mercury use structural equivalence. So for recursive
type synonyms, it does make sense to consider the type as equivalent
to its unrolling. That's why I think it's reasonable to describe
recursive synonym types as infinite types.
Fergus Henderson
>f...@cs.mu.oz.au (Fergus Henderson) writes:
>
>>So although it's true that any value which you can completely specify
>>with Haskell must come from a countabe set, it's not true that all
>>values which can be *used* in Haskell programs must come from a
>>countable set.
>
>It depends what you mean by 'used'.
>
>I would say: any value you use in a Haskell program must take a finite
>amount of memory. Otherwise the program would never terminate (any
>terminating TM uses a finite amount of space).
The Haskell Report does not require Haskell programs to terminate.
Also, Haskell programs are run on real computers, not on Turing
machines. Real computers provide sources of randomness, such as disk
drive seek times, that are based on physical phenonoma which can not
necessarily be accurately modelled using Turing machines.
Fergus Henderson
>As a matter of fact, your "r", when seen as a real number, is not
>really a value because it will never be fully realized.
Well, that depends on what you mean by "value" (and "real" ;-).
I think it is certainly quite reasonable use of language
to say that `r' has a value, even though the program never
completely computes that value.
Edward Avis
>>I would say: any value you use in a Haskell program must take a finite
>>amount of memory. Otherwise the program would never terminate (any
>>terminating TM uses a finite amount of space).
>
>The Haskell Report does not require Haskell programs to terminate.
Okay... but it still must use a finite amount of memory on any real
computer. Unless you are in there frantically adding more RAM chips
while your program executes :-)
>Also, Haskell programs are run on real computers, not on Turing
>machines. Real computers provide sources of randomness, such as disk
>drive seek times, that are based on physical phenonoma which can not
>necessarily be accurately modelled using Turing machines.
But Haskell doesn't provide any way to get this randomness into a
value (apart maybe from unsafePerformIO). The best you can do is to
put things into the IO monad, and construct an 'IO object' which given
one state of the world, performs actions to turn it into another state
of the world.
If you have something like
main = (hGetContents stdin) >>= (\x -> ... x ...) >>= putStr
then you haven't really given x a value at all. All you have said is
what to do with whatever string comes from stdin (which, if we allow
infinitely long inputs, is an uncountable number of inputs).
The function main, which is the only thing you've actually given a
value, has just one possible value.
--
Ed Avis
ep...@doc.ic.ac.uk
Matthias Blume
> Also, Haskell programs are run on real computers, not on Turing
> machines. Real computers provide sources of randomness, such as disk
> drive seek times, that are based on physical phenonoma which can not
> necessarily be accurately modelled using Turing machines.
But they can be modelled by other means, for example using a
ficticious pre-existing stream of random bits. A randomized program
is then nothing more than a deterministic program with an additional
parameter.
Matthias Blume
> >As a matter of fact, your "r", when seen as a real number, is not
> >really a value because it will never be fully realized.
>
> Well, that depends on what you mean by "value" (and "real" ;-).
... and "and". :-)
> I think it is certainly quite reasonable use of language
> to say that `r' has a value, even though the program never
> completely computes that value.
Reasonable in certain contexts (teaching, handwaving, ...), but not
when you are dealing with semantics of PLs.
Daniel C. Wang
> I don't agree. Mercury, Haskell and most other functional languages
> use name equivalence rather than structural equivalence for
> user-defined algebraic types. If in Mercury I write
>
> :- type foo ---> f(list(foo)). % This Mercury syntax
> % means the same as the
> % Haskell example above
> :- type bar ---> f(list(bar)).
>
> then the infinite type trees that you would get by unrolling the
> definitions for `foo' and `bar' would be the same:
> `f(list(f(list(f(list(...))))))'. But because the language uses name
> equivalence rather than structural equivalence, the two types are
> distinct. This shows that you can't just treat a recursive type as
{stuff deleted}
This is my point, there is a well defined theory of recursive types based
completely on structural equivalence. There are O(n^2) algorithms for deciding
whether two recursive types are structurally subtypes of each other. The
only reason there is a difference is because most languages adopt name
equivalence rather than structural equivalence. This is purely a pragmatic
issue. The underlying theory doesn't make any real distinction.
(I'm complianing about this because, I just spent the last few weeks reading
way too much background theoretical litterature on the subject of subtyping
and recursive types.)
To be honest there is some distinction one could probably make that is
similar to the "recursive" vs. "infinite" argument. In the litterature this`
is close to the "iso-recursive" vs. "equi-recursive" interpretation of
recursive types. In the iso-recursive theories you talk about the
equivalence of finite unfoldings and provide operators "fold" and "unfold"
to either unfold the type one level more or to do the opposite. Or to say it
another way types are equivalent if there is some isomorphism between them
that can be constructed with the "fold" and "unfolds". The explicit data
constructors are implicitly using the "fold" and "unfolds". (Some times
called "roll" and "unroll" too...)
In the equi-recursive interpretation each type is just some possibly infinite
tree. The types are the same if the possibly infinite trees are the same.
"same" in the sense that a tree is really just a set in a pure mathematical
sense. So if the the inifite sets are the same the types are the same. This
usally invovles the use of a "co-induction" principal which I don't
completely understand. I will have to spend a few more weeks rereading the
papers before it all sinks in.... then maybe I'll get to graduate... :)
Fergus Henderson
>f...@cs.mu.oz.au (Fergus Henderson) writes:
>
>>Also I think you missed the distinction between value and
>>representation. [...]
>>The representation at any given point in time is finite, but the value
>>is infinite.
>
>I think I get it now. But if we are doing Haskell _programming_,
>rather than just using Haskell as a way of representing functions,
>then it is only the representations which are important.
Here I'd have to disagree again. A big part of the process of
programming is _reasoning about programs_. And when reasoning about
Haskell programs, it's usually a lot easier to reason about the values
rather than reasoning about the representations. So values certainly
are important.
>You can't
>input or output any value unless you can find a representation for
>it. And you can't fully compute it either.
I agree with those statements.
>>>- If I do not interrupt the program, it never terminates
>>>and thus does not produce a result at all.
>>
>>Here I disagree. If you were to say instead that it doesn't
>>ever produce a _complete_ result, I'd agree.
>
>Okay, we'll go with what you say, that it produces a _partial_ result.
Well, not quite. It produces an unending sequence of partial results,
rather than just producing a single partial result.
>This partial result must be a finite list. The finite lists of Bool
>are countable.
That's true, but unending sequences of finite lists of Bool
are not countable.
>I think that distinguishing between values and representations has
>probably cleared up the confusion?
I think so. What remains is just some disagreement about terminology.
Fergus Henderson
>f...@cs.mu.oz.au (Fergus Henderson) writes:
>
>> Also, Haskell programs are run on real computers, not on Turing
>> machines. Real computers provide sources of randomness, such as disk
>> drive seek times, that are based on physical phenonoma which can not
>> necessarily be accurately modelled using Turing machines.
>
>But they can be modelled by other means, for example using a
>ficticious pre-existing stream of random bits. A randomized program
>is then nothing more than a deterministic program with an additional
>parameter.
OK, but the set of possible outputs of nonterminating programs whose
inputs includes an infinite stream of random bits is uncountable.
This contrasts with the set of possible outputs of finite programs
with finite input, which is countable.
Fergus Henderson
>f...@cs.mu.oz.au (Fergus Henderson) writes:
>
>> I don't agree. Mercury, Haskell and most other functional languages
>> use name equivalence rather than structural equivalence for
>> user-defined algebraic types. If in Mercury I write
>>
>> :- type foo ---> f(list(foo)).
>> :- type bar ---> f(list(bar)).
>>
>> then the infinite type trees that you would get by unrolling the
>> definitions for `foo' and `bar' would be the same:
>> `f(list(f(list(f(list(...))))))'. But because the language uses name
>> equivalence rather than structural equivalence, the two types are
>> distinct. This shows that you can't just treat a recursive type as
>{stuff deleted}
>
>This is my point, there is a well defined theory of recursive types based
>completely on structural equivalence. There are O(n^2) algorithms for deciding
>whether two recursive types are structurally subtypes of each other. The
>only reason there is a difference is because most languages adopt name
>equivalence rather than structural equivalence. This is purely a pragmatic
>issue. The underlying theory doesn't make any real distinction.
If the languages use name equivalence, then why is the existance of
a theory of recursive types based completely on structural equivalence
relevant?
You're arguing that the distinction I'm making between infinite types
and recursive types is not valid, because it doesn't hold in this theory;
but the distinction _is_ valid for the languages I'm talking about,
and the fact that this theory uses structural equivalence just means
that using that theory to model those languages won't work.
Fergus Henderson
>f...@cs.mu.oz.au (Fergus Henderson) writes:
>
>>>I would say: any value you use in a Haskell program must take a finite
>>>amount of memory. Otherwise the program would never terminate (any
>>>terminating TM uses a finite amount of space).
>>
>>The Haskell Report does not require Haskell programs to terminate.
>
>Okay... but it still must use a finite amount of memory on any real
>computer. Unless you are in there frantically adding more RAM chips
>while your program executes :-)
Who says it has to be done frantically? ;-)
>>Also, Haskell programs are run on real computers, not on Turing
>>machines. Real computers provide sources of randomness, such as disk
>>drive seek times, that are based on physical phenonoma which can not
>>necessarily be accurately modelled using Turing machines.
>
>But Haskell doesn't provide any way to get this randomness into a
>value (apart maybe from unsafePerformIO). The best you can do is to
>put things into the IO monad, and construct an 'IO object' which given
>one state of the world, performs actions to turn it into another state
>of the world.
>
>If you have something like
>
>main = (hGetContents stdin) >>= (\x -> ... x ...) >>= putStr
>
>then you haven't really given x a value at all. All you have said is
>what to do with whatever string comes from stdin (which, if we allow
>infinitely long inputs, is an uncountable number of inputs).
>
>The function main, which is the only thing you've actually given a
>value, has just one possible value.
I agree with all of that.
But, for any given initial state of the world, if the program is
executed with that initial state of the world, then `x' will have some
value (initially represented as an unevaluated closure), and the
program will use that value (forcing the closure to be evaluated to
WHNF). The set of possible values which `x' can take is uncountable.
So if we go back to the original question, which IIRC was something
along the lines of "is the set of values which can be used in a
Haskell program countable?", I would still answer "no".
If the question was worded differently then my answer might change.
graham
>This is my point, there is a well defined theory of recursive types based
>completely on structural equivalence. There are O(n^2) algorithms for deciding
>whether two recursive types are structurally subtypes of each other.
Can anyone supply a pointer to these algorithms?
thanks
graham
Daniel C. Wang
> a theory of recursive types based completely on structural equivalence
> relevant?
>
> You're arguing that the distinction I'm making between infinite types
> and recursive types is not valid, because it doesn't hold in this theory;
> but the distinction _is_ valid for the languages I'm talking about,
> and the fact that this theory uses structural equivalence just means
> that using that theory to model those languages won't work.
If Turing machines and Haskell programs are the same why are Haskell
programs relevant? I'm not claiming that Haskell programs or recursive types
are irrelevant. I'm just saying that when you stand back really far enough
the difference between the two is not as big as you think. Just like the
fact that if you stand back far enough you see that there's really "no
difference" between Turing machine programs and Haskell programs.
I'm not saying there is no difference. Just that the differences are
pragmatic and aren't "fundamental". No matter how far you stand back a DFA
isn't a TM. But a two tape TM and a one tape TM are really "the same". A
program for a two tape TM and a one tape TM are different but really they
are "the same". Likewise for "recursive" and "infinite" types. They are
really the same in power, any differences are just issues of notation.
Daniel C. Wang
graham <grah...@telocity.com> writes:
Efficient recursive subtyping, with Dexter Kozen and Michael
I. Schwartzbach. Mathematical Structures in Computer Science,
5(1):113-125, 1995. Preliminary version in Proceedings of POPL'93,
Twentieth Annual SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, pages 419-428, Charleston, South Carolina, January 1993.
which can be found at
http://www.cs.purdue.edu/homes/palsberg/paper/mscs95-kps.ps.gz
Jens Palsberg has a student who has a slightly stronger result that handles
associative and commutative type constructors
http://www.cs.purdue.edu/homes/tzhao/isomorphism/tech-report.ps
I think this result will be published soon... he also has a nice biblography
on recursive type isomorphism on the web..
http://www.cs.purdue.edu/homes/tzhao/ref.html
(BTW Google is an amazingly useful research tool if you know the right buzz
words .... www.google.com)
graham
> Efficient recursive subtyping, with Dexter Kozen and Michael
> I. Schwartzbach. Mathematical Structures in Computer Science,
> 5(1):113-125, 1995. Preliminary version in Proceedings of POPL'93,
> Twentieth Annual SIGPLAN-SIGACT Symposium on Principles of Programming
> Languages, pages 419-428, Charleston, South Carolina, January 1993.
>
> which can be found at
>
> http://www.cs.purdue.edu/homes/palsberg/paper/mscs95-kps.ps.gz
>
Thanks for the references.
graham
Matthias Blume
> Matthias Blume <s...@my.sig> writes:
>
> >But they can be modelled by other means, for example using a
> >ficticious pre-existing stream of random bits. A randomized program
> >is then nothing more than a deterministic program with an additional
> >parameter.
>
> OK, but the set of possible outputs of nonterminating programs whose
> inputs includes an infinite stream of random bits is uncountable.
Well, yes, if you assume the existence of an uncountable domain D,
take a value v \in D from it, and apply the identity function to that
value v, then you obviously have an output domain that is also
uncountable.
However, the uncountability here is entirely due to the (unnecessary)
assumption that an input domain is uncountable. The assumption is
unnecessary because every finite prefix of the output (and those are
the only ones that matter) can be obtained by considering only finite
prefixes of the input. Finite prefixes are countable, and using this
approach everything is back to the "computable functions and their
domains are countable" common wisdom.
Now, you are probably going to say that my "those are the only ones
that matter" assertion is questionable. But until you show me a
Turing machine (or a program for a real computer, for that matter)
that actually intrinsically depends on its input stream being infinite
as opposed to simply "long enough", I will stand by that assertion.
Markus Mottl
> However, the uncountability here is entirely due to the (unnecessary)
> assumption that an input domain is uncountable. The assumption is
> unnecessary because every finite prefix of the output (and those are
> the only ones that matter) can be obtained by considering only finite
> prefixes of the input. Finite prefixes are countable, and using this
> approach everything is back to the "computable functions and their
> domains are countable" common wisdom.
You mean that the important thing actually is that a function be finitary,
which is equivalent to being continuous. The latter (continuity) is, of course,
a necessary requirement for a function to be computable.
It is indeed unimportant from which source domain (countable or not) you map to
which target domain: as long as the function does it in a continuous way, it is
computable.
That's the reason why you can have arbitrary precision *real* arithemetic:
there is no need to look at an infinite amount of data (digits) if you only
want to have a finite amount of output (given precision / number of digits).
Therefore, there must be a computable function that can do this...
Regards,
Markus
--
Markus Mottl, mo...@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl