> 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
On 25-Feb-1999, Carl R. Witty <[EMAIL PROTECTED]> wrote:
> Fergus Henderson <[EMAIL PROTECTED]> writes:
>
> > 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 rea
On 25-Feb-1999, Nick Kallen <[EMAIL PROTECTED]> wrote:
>
> I'm not asking the compiler to deduce anything. I'm talking about run-time
> type matching; this is dynamic types!
Hmm, that seems to be different to what you said last time.
Let me quote:
[Nick Kallen:]
> [Fergus:]
> 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 strange. If there are no principal types
(which we can't hope for), then user added signatures can
have the effect of changing
I have found another useful application of types with value parameters in
C++. I have seen an example of using types to check for proper use of
physical units. I have found this very useful. But I haven't found a way to
express this in haskell. It would be nice to have a type system, that
supports
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, t
On 24-Feb-1999, John C. Peterson <[EMAIL PROTECTED]> wrote:
> You can't nuke monomorphism without addressing the ambiguity problem.
If you've got the time, would you mind giving an example of the kind
of ambiguity you're talking about? I think I know roughly the kind
of problem you're talking ab
On 24-Feb-1999, Thomas Hallgren <[EMAIL PROTECTED]> wrote:
> I agree with Johns objection to the compiler warning solution, so here is
> another suggestion:
>
> The monomorphism restriction makes sure that certain values are computed
> at most once by restricting them to be used at only one type.
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 Pa
> > > 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 strange. If there are no principal types
> > (which we can't hope for), then user added signatures can
> > have
Leon Smith <[EMAIL PROTECTED]> wrote (about a week ago):
> [...]
> With dependent types, would it be possible to get types from values (i.e.
> types that you haven't actually declared before.) One example would be the
> group of integers modulo n. It sounds to me like types would then be firs
[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
"Nick Kallen" <[EMAIL PROTECTED]> writes:
> > 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
"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
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
Folks,
the postmaster here at Glasgow is starting to complain about the load
that this list is starting to have on the mail setup. So, may I
suggest that people have a look at the mailing list archives to
orientate themselves about the issues and arguments surrounding the MR
before generating mo
> 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 th
On 24-Feb-1999, John Hughes <[EMAIL PROTECTED]> wrote:
>
> Everybody agrees the monomorphism restriction is a pain: [...]
> On the other hand, interpreting such definitions using call-by-name when the
> programmer expects call-by-need would REALLY introduce a trap for the unwary.
>
> Some sugges
Lennart Augustsson <[EMAIL PROTECTED]> writes:
> One solution, admittedly somewhat of a hack, is to be able
> to mark one of the components of a record as being the
> essential one. E.g.
> sort :: (l :: [a]) -> sig { *r :: [a]; s :: Sorted l r }
> where the * marks the essential component. Th
Fergus Henderson <[EMAIL PROTECTED]> writes:
> > It is, however, also clear that when in using dependant types, much more
> > type information and documentation are provided. If, in fact, the example
> > from above can be type checked (question [2]), then it is clear that
> > dependant types are
> > > 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 li
> 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 i
> 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 typ
Lennart Augustsson <[EMAIL PROTECTED]> writes:
> Let me just point out that my main interest in dependent types is
> NOT to do specifications and proofs (like sort above), but to
> make the type system more expressible. This way we can make more
> programs typeable, and also give more accurate t
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 progra
Joe English:
> I was thinking of the example from the Haskell Report:
>
> let { len = genericLength xs } in (len, len)
>
> which, without the MR, computes 'len' twice.
> Operationally I expect that in "let x = f y in ... x ... x",
> 'f y' is only evaluated once, no matter what type it is.
26 matches
Mail list logo
