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
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.
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.
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
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
> 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
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
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
> 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
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:]
> > > 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
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
"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
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 Pa
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
> 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
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
> 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
[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
> 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
> > > 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
"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
26 matches
Mail list logo
