On 28-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote:
I downloaded the NU-Prolog manual and skimmed it, but I didn't see the
features you're describing (probably because I haven't "done" Prolog
since my learn-5-languages-in-a-quarter class 12 years ago). Could
you give me a pointer to
Lennart Augustsson [EMAIL PROTECTED] writes:
(I believe that there are type
theories with dependent types, such as the one in Thompson's _Type
Theory and Functional Programming_, where each term has at most one
type; so it can't just be dependent types that disallow principal
types.)
Fergus Henderson [EMAIL PROTECTED] writes:
Could you give an example of language syntax that you feel would be
better than putting these properties in the type system, while still
allowing similar compile-time checking?
I already gave NU-Prolog and Eiffel as examples.
Those languages
On 26-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote:
This occurs because in the absense of type declarations,
Haskell assumes that any recursion will be monomorphic,
which is in general not necessarily the case.
As I'm sure you know, type inference is in general impossible
for
On 25-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote:
[someone wrote:]
I've lost track of what we're talking about here. In what system can
we not hope for principal types?
[...] Cayenne doesn't have that property.
Again, I think this is a feature, not a bug. I'll include
a
So what does Cayenne do if you don't declare the type for `push'?
Does it report an error?
The basic principle in Cayenne is that you need type signatures
everywhere. This is sometimes rather verbose and is relaxed
in some cases, but not here. If you omit the type signature
the compiler
On 25-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote:
Fergus Henderson [EMAIL PROTECTED] writes:
Certainly a language with dependent types should define exactly what
types the type checker will infer. But when generating code, the
compiler ought to be able to make use of more accurate
This occurs because in the absense of type declarations,
Haskell assumes that any recursion will be monomorphic,
which is in general not necessarily the case.
As I'm sure you know, type inference is in general impossible
for polymorphic recursion, and since Haskell insists on
decidable type
The key issue in Lennart's example, I think, is monomorphic recursion.
For the function
f _ =
let y = f 'a'
in undefined
Haskell incorrectly (IMHO) infers the type `f :: Char - a'
instead of the more general type `f :: b - a'.
This occurs because in the absense
Nick Kallen [EMAIL PROTECTED] writes:
You cannot do this in Cayenne, there are no operations that scrutinize
types. They can only be built, and never examined or taken apart.
This is a deliberate design choice. The consequence is that type
cannot affect the control of a program, so
Watch out here; there may be a limit to how much run-time type
inspection it is reasonable to do in the presence of dependent types.
Suppose you're examining a type which happens to be the type of some
sorting function:
(Ord a) = (l :: [a]) - ((l' :: [a]), sorted l l')
How much type
On 24-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote:
Fergus Henderson [EMAIL PROTECTED] writes:
What if the body of min2 were defined so that it returned
something different in the two cases? Your code has no proof that the
code for the two cases is equivalent. If it's not, then the
On 24-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote:
Fergus Henderson [EMAIL PROTECTED] writes:
What if the body of min2 were defined so that it returned
something different in the two cases? Your code has no proof that the
code for the two cases is equivalent. If it's not, then
If this is true, then what I'm doing is horrible. But I don't
see how this
leads to nondeterminism or broken referential transparency.
min2 returns the
same value for the same list, but it's simply more efficient
if we happen to
know some more information about the list.
In
Fergus Henderson [EMAIL PROTECTED] writes:
Certainly a language with dependent types should define exactly what
types the type checker will infer. But when generating code, the
compiler ought to be able to make use of more accurate type information,
if it has that information available,
Fergus writes:
I think it's becoming clear by now that the theoretical disadvantages
of undecidable type checking are often not significant in practice.
Experience with C++, Gofer, ghc, Mercury, etc. all seems to confirm this.
In this context, people may find the paper _C++ Templates as
I don't understand. What behaviour is different here?
Certainly the type is different. But how is the behaviour different?
It behaves differently in that it accepts and returns more/less values. If
this function is part of a program, then the behavior of the program is now
different in that
[Resend - mlist trouble; apologies if you've already
received it. -moderator]
Lennart Augustsson [EMAIL PROTECTED] writes:
2) Yes, I agree that the possibility that user-supplied type
declarations can change the meaning of the program is a strike against
the idea.
I don't find that so
I've lost track of what we're talking about here. In what system can
we not hope for principal types? (I believe that there are type
theories with dependent types, such as the one in Thompson's _Type
Theory and Functional Programming_, where each term has at most one
type; so it can't
"Nick Kallen" [EMAIL PROTECTED] writes:
If this is true, then what I'm doing is horrible. But I don't
see how this
leads to nondeterminism or broken referential transparency.
min2 returns the
same value for the same list, but it's simply more efficient
if we happen to
know
[EMAIL PROTECTED] writes:
[EMAIL PROTECTED] writes:
enabling types to express all properties you want is, IMO, the right way.
Why do I feel that there must be another approach to programming?
How many people do you expect to program in Haskell once you are done adding all
it takes to
On 22-Feb-1999, Nick Kallen [EMAIL PROTECTED] wrote:
min2 :: [a] - a
min2 ((l:ls) :: [a] = Sorted) = l
min2 l = min l
What's the semantics of that supposed to be?
If the list is not known to be definitely sorted,
will it check sortedness at runtime?
If not, then the semantics could be
On 21-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote:
(i.e., you leave out the pivot [x])
Obviously the result of sort will no longer be a permutation of its
argument. Will this then not type check?
No, the proof (whereever it is) would no longer type check.
As I understand
On 21-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote:
F a * = member (map (F a) [0..]) // member [a] a - Bool
I mave no clue what this means. What is `member'?
Member is memq, in, etc. Checks for membership in a list.
I'm still lost. What is // and how does it bind?
I
If you return the same proof of correctness that you used
for the earlier definition of sort, then no it won't type check.
But if you return a proof defined as e.g.
proof = proof
then if I understand things correctly it will type check.
On that note, since this has been of
No, the proof (whereever it is) would no longer type check.
As I understand it, this is not necessarily true:
if the proof contains loops, it might type check,
even though it is not really a valid proof.
You're right. If the proof is looping it will still
pass as a proof.
--
apply :: (F a *) [a] - (F a *)
apply f [] = a
apply f [a:as] = apply (f a) as
The type gets noisier.
(To correct a couple of minor typos, that should be
apply f [] = f
apply f (a:as) = apply (f a) as
)
Heh, thank you. :)
I agree it is in some sense six of one and
I consider even the second one to be mixing the proofs
with the code, because there's no easy way that I can tell at
a glance that `sortReallySorts' is a proof rather than a program.
But I consider that a feature and not a bug. :-)
-- Lennart
[EMAIL PROTECTED] wrote:
enabling types to express all properties you want is, IMO, the right way.
Why do I feel that there must be another approach to programming?
How many people do you expect to program in Haskell once you are done adding all
it takes to "express all imaginable
...I thought about this pretty hard. Particularly I thought about using
classes; this was fruitless. So I decided I'd invent a new language feature
and a nice little syntax to handle it.
Sorted l r = Ordered r /\ Permutation l r
sort :: (l :: [a]) - (r :: [a]) = Sorted l r
You've
On 20-Feb-1999, Nick Kallen [EMAIL PROTECTED] wrote:
[Lennart wrote:]
[Nick Kallen wrote:]
To what
extent will a program that type checks completely fail to follow its
specification? Can someone give specific examples?
It's trivial to construct examples. Take sorting
sort ::
The basic problem that I have with this is that although dependent types
do allow you to specify a lot of things in the type system, I'm not sure
that using the type system is really the best way to specify these things.
Well, I think types are just the place for these things. People already
On 19-Feb-1999, Nick Kallen [EMAIL PROTECTED] wrote:
I'll admit to not having yet written something in Cayenne, but I'm an
adamant supporter of adding dependant types to the language. I remember a
year ago, I was writing a small (trivial) program. One of the essential ways
I was structuring
[EMAIL PROTECTED] writes:
enabling types to express all properties you want is, IMO, the right way.
Why do I feel that there must be another approach to programming?
How many people do you expect to program in Haskell once you are done adding all
it takes to "express all imaginable properties
Well if the ComplicatedTypeToSpecifySorting is correct (I don't know if
this is possible, but I suspect it isn't) it will of course not type check.
Of course it is possible. The types in Cayenne have the same power
as predicate logic, so you can specify most anything you like.
Here's a
F a * = member (map (F a) [0..]) // member [a] a - Bool
I mave no clue what this means. What is `member'?
Member is memq, in, etc. Checks for membership in a list.
I'm still lost. What is // and how does it bind?
This is how I parse it:
(member (map (F a) [0..])) // ( (member [a] a)
Well, yes, up to a point, but it may be clearer if the simple
regular types part is kept separate from the undecidable part,
as was done in NU-Prolog, or as is done in Eiffel.
I'm not necesssarily advocating that the properties and proofs of these
properties should be mixed with the regular
On 21-Feb-1999, Lennart Augustsson [EMAIL PROTECTED] wrote:
[Fergus wrote:]
The basic problem that I have with this is that although dependent types
do allow you to specify a lot of things in the type system, I'm not sure
that using the type system is really the best way to specify these
Nick Kallen [EMAIL PROTECTED] wrote:
apply f (p:ps) = apply (f p) ps
apply f [] = f
I wanted to express the type as something like:
apply :: (a - a - ... - a) [a] - a
No, that's not what you want. :-) You want
apply :: (a - a - ... - b) [a] - b
I think the distinction is important
I wanted to express the type as something like:
apply :: (a - a - ... - a) [a] - a
No, that's not what you want. :-) You want
apply :: (a - a - ... - b) [a] - b
I think the distinction is important (see below).
F a * = member (map (F a) [0..]) // member [a] a - Bool
I mave no
If your language supports optional dynamic type checking, as it should,
then expressing functions like apply shouldn't be too hard.
Here's a dynamic apply in a pseudo Clean 2.0 syntax:
apply :: Dynamic [a] - a
apply (f :: a - b) (arg:args) = apply (dynamic (f arg) :: b) args
apply (f :: a) []
OK, I'm curious. Two people replied that C++ has undecidable type
checking. I was not aware of this (although I can't say I'm too
surprised); do you have a reference?
It's actually the template processing that can loop, but it is
sort of part of the type checking.
You can find an article
On 18-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote:
OK, I'm curious. Two people replied that C++ has undecidable type
checking. I was not aware of this (although I can't say I'm too
surprised); do you have a reference?
Not really. I believe this has been mentioned on comp.std.c++,
but I
Lennart Augustsson writes:
OK, I'm curious. Two people replied that C++ has undecidable type
checking. I was not aware of this (although I can't say I'm too
surprised); do you have a reference?
It's actually the template processing that can loop, but it is
sort of part of the type
I'm curious: how many people have actually written a program in
Cayenne? How many people have written programs that made significant
use of the dependent typing? Has anybody tried to teach a programming
class using Cayenne?
I'll admit to not having yet written something in Cayenne, but I'm
On Wed, 17 Feb 1999, George Beshers wrote:
1. If the tool can resolve the types (and I would expect this
to be true most of the time) it can display the types and (if
the user or style guide dictates) add the types to the source.
2. If the tool can not resolve the type of a particular
I'm not sure that anybody has "accepted"
undecidable type checking.
People using Gofer or C++ seem to have.
-- Lennart
2.in the face of the above, we need to give the compiler more guidance.
Personally, I favour type declarations everywhere: all identifiers should be
introduced as being of a particular specified type.
Of course, whether these principles are compatible with Haskell it another
On Wed, 17 Feb 1999, michael abbott wrote:
As a C++ user (with a background in categories) patiently waiting for
something a lot better, I personally favour two principles:
1.let's go for undecidable type checking. I want the compiler to be able
to do as much work as possible: ideally,
are compatible with Haskell it another
question...
-Original Message-
From: Lennart Augustsson [mailto:[EMAIL PROTECTED]]
Sent: 17 February 1999 10:26
To: [EMAIL PROTECTED]
Cc: [EMAIL PROTECTED]; [EMAIL PROTECTED];
[EMAIL PROTECTED]
Subject: Re: Haskell 2 -- Dependent types?
I'm not sure
On 16 Feb 1999, Carl R. Witty wrote:
Lars Lundgren [EMAIL PROTECTED] writes:
We have already accepted undecidable type checking, so why not take a
big step forward, and gain expressive power of a new magnitude, by
extending the type system to allow dependent types.
Wait a
On 16-Feb-1999, Carl R. Witty [EMAIL PROTECTED] wrote:
I'm not sure that anybody has "accepted" undecidable type checking.
I think it's becoming clear by now that the theoretical disadvantages
of undecidable type checking are often not significant in practice.
Experience with C++, Gofer, ghc,
Alexander Jacobson [EMAIL PROTECTED] writes:
* facilitate better integration with other languages/systems
For example, it would be nice to be able either to generate a Haskell
datatype from an XML DTD or to generate a XML DTD from a Haskell
datatype.
Funnily enough, that's exactly what
Alexander Jacobson [EMAIL PROTECTED] writes:
* facilitate better integration with other languages/systems
For example, it would be nice to be able either to generate a Haskell
datatype from an XML DTD or to generate a XML DTD from a Haskell
datatype.
Funnily enough, that's exactly
I read cayenne.ps and it went somewhat over my head.
I could not get a good sense of when in practice I would really want to use
this. This is not an objection, just a request for explanation...
As far as the type system goes, what would be more useful to me is
something preprocessor
Lars Lundgren [EMAIL PROTECTED] writes:
We have already accepted undecidable type checking, so why not take a
big step forward, and gain expressive power of a new magnitude, by
extending the type system to allow dependent types.
Wait a minute...who has accepted undecidable type checking?
56 matches
Mail list logo
