Re: Original naming

[Simon L Peyton Jones <simonpj@cs.glasgow.ac.uk>]

To: "David J. McNally" <djm@cs.st-and.ac.uk>
Cc: haskell@cs.glasgow.ac.uk, simonpj@cs.glasgow.ac.uk
Subject: Re: Original naming 
Date: Wed, 28 Nov 90 17:38:40 +0000
From: Simon L Peyton Jones <simonpj@cs.glasgow.ac.uk>
Sender: haskell-request@cs.glasgow.ac.uk



| Consider the following example :
| 
| 	module A where
| 	data T = X Bool
| 
| in one "file"
| 
| 	module B(f) where
| 	import A
| 	f (X b) = b

So B has an interface looking like this:

	interface B
	import A(T)
	f :: T -> Bool


| ... (omitted stuff) ...
| yield an executable program as a result which behaves as expected.  Now con
|  sider a new implementation of module A :-
| 
| 	module A where
| 	data T = X Int
| which is compiled separately .... no problem so far ...
| now we can define a new Main :-
| 
| 	module Main where
| 	import A
| 	import B
| 	main resps = [ AppendChan stdout (show (f (X 3))) ]
| 
| which should compile correctly yielding an executable program.  Why?
| Because T has the same original name in both the original implementation
| of A and the new one - namely ("A","T") so function f can be applied to
| objects of this type regardless of which A they come from. The result
| is that objects of any type can effectively be turned into objects of
| another type.  That is, the system is not type safe. 

| ... omitted...
| Have these problems occurred to the language designers?  If so, what do
| they propose to do about them?


Absolutely they have.  The Report very carefully defines what it means for
an interface to be "consistent" with an implementation (section 5.3.1).  In
particular, once you have changed A, and hence A's interface, the
implementation of B is no longer consistent with its interface.  The new
interface is

	interface B
	import A(T)
	f :: T -> Int

The Report also states (section 5.1.4) that "the task of checking 
consistency between interfaces and implementations must be done by the
compilation system".

The Report defines the meaning of a collection of modules and interfaces
provided they are consistent.  If they aren't consistent, the meaning of
the program is not defined.

This is no more an "external agency" (which Dave objects to) than the
compiler itself.  It is required that the compiler check each module
for type correctness before running the program, and Dave does not
object to that.  All that is being said is that in addition the consistency
of each implementation with its interface must be checked.  This seems
fair enough to me.

Simon