Miranda's Type System 
Author Message
 Miranda's Type System

Fooling arounf with Miranda (tm), version 1.016, I discovered the following
oddity about the type system.  Define the following two functions:

  f x = x + g
  h y = y:g

It is easy to see that in the first  g  must have the type  num
and in the second  g  must have the type  [*], but all Miranda does
is to issue you with a WARNING that  g  is undefined.  Because of lazy
evaluation it is now possible to evaluate, eg:

  hd (h 2)

and Miranda replies with  2.  I'd prefer a type discipline that does
not allow the above two function definitions to pass through the
type-checker.  Does anyone agree?



Thu, 10 Dec 1992 22:22:42 GMT  
 Miranda's Type System

Quote:
>Fooling arounf with Miranda (tm), version 1.016, I discovered the following
>oddity about the type system.  Define the following two functions:
>  f x = x + g              h y = y:g
>It is easy to see that in the first  g  must have the type  num
>and in the second  g  must have the type  [*], but all Miranda does
>is to issue you with a WARNING that  g  is undefined.  Because of lazy
>evaluation it is now possible to evaluate, eg:      hd (h 2)
>and Miranda replies with  2.  I'd prefer a type discipline that does
>not allow the above two function definitions to pass through the
>type-checker.  Does anyone agree?

I agree !

But Miranda version 2.009 doesn't accept the above function definitions.
You get an 'UNDEFINED NAME' error for g instead of a warning.
You can't evaluate hd (h 2) then, because h couldn't be defined.
Try to avoid undefined names in older Miranda versions (think ERROR everytime
you see the word WARNING) or use a more recent version.

Andreas



Sat, 12 Dec 1992 17:11:54 GMT  
 Miranda's Type System


Quote:
Diller <DillerAR>) writes:

|>>Fooling arounf with Miranda (tm), version 1.016, I discovered the following
|>>oddity about the type system.  Define the following two functions:
|>>  f x = x + g              h y = y:g
|>>     [couple of lines deleted]
|>>Under lazy evaluation it is now possible to evaluate, eg:      hd (h 2)
|>>and Miranda replies with  2.  I'd prefer a type discipline that does
|>>not allow the above two function definitions to pass through the
|>>type-checker.  Does anyone agree?
|>
|> I agree !

I agree that it would be nice to have this flagged as an error and thus be
prevented from using f or g *but* I don't agree that this is a fault in the
type discipline.

For example, define p and q,

p x = x + g                   q x = x & g
      where                         where
      g = f x                       g = h x

In p both the inferred and actual type of g is num, whilst in q the inferred
type is bool but the actual type is [*].

The type of p is correct because although g is undefined, it is used
consistently throughout the defintion. However, I would like the system to
reject p because it is not completely defined.

|> But Miranda version 2.009 doesn't accept the above function definitions.
|> You get an 'UNDEFINED NAME' error for g instead of a warning.
|> You can't evaluate hd (h 2) then, because h couldn't be defined.

Hmmm.. we have version 2.009 and both definitions get through with only
a warning, and can evaluate hd (h 2). Our system is running on a SUN 3, what
about yours ?

Paul.

"I was dreaming when I wrote this, forgive me if it goes astray"

                       Paul Sanders



Sat, 12 Dec 1992 22:57:04 GMT  
 
 [ 3 post ] 

 Relevant Pages 

1. Miranda's Types

2. Difference between a type system and a type constraint system

3. Difference between a type system and a type constraint system

4. Biff's-own-guide to type systems?

5. An Attempt to Formalise Dylan's Type System (Part 2)

6. An Attempt to Formalise Dylan's Type System (Part 1)

7. Dylan's type system

8. Dylan's type system

9. type systems and #f and '()

10. Visual Prolog's type system

11. Wanted: parser for typed lambda calc in Miranda

12. Miranda system needed for PC

 

 
Powered by phpBB® Forum Software