Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!caen!ox.com!math.fu-berlin.de!opal!wg
From: wg@opal.cs.tu-berlin.de (Wolfgang Grieskamp)
Newsgroups: comp.lang.misc
Subject: Re: Dynamic typing (part 3)
Keywords: type inference static dynamic lisp ml
Message-ID: <3183@opal.cs.tu-berlin.de>
Date: 30 Apr 91 02:52:26 GMT
References: <boehm.670539603@siria> <1991Apr9.021700.2688@neon.Stanford.EDU> <3092@opal.cs.tu-berlin.de> <1991Apr22.234707.7023@neon.Stanford.EDU>
Sender: news@opal.cs.tu-berlin.de
Reply-To: wg@opal.cs.tu-berlin.de
Followup-To: comp.lang.misc
Organization: Technical University of Berlin
Lines: 51
Nntp-Posting-Host: troll

[Excuse me, but this is somehow out of time...]

brm@neon.Stanford.EDU (Brian R. Murphy) writes:

 >I fail to see how parameterization is relevant.  But yes, the case of
 >of a possible error value _is_ a more common case of my example.  For
 >example, a Lisp expression such as
 >	(if (= y 0) (error) (/ x y))
 >would have type [something like] (error + int).  So either we must
 >automatically include errors in every base type, introduce an explicit
								^^^^^^^^
 >union declaration in just about every function, or complicate things a
 >bit by going to a continuation-passing semantics.  Other examples
 >besides errors _do_ come up, though, so why not just adopt a more
 >general solution?

Yes, why not? The general solution (for this class of problems) may
be "anonymous unions". For the example, its inferrable.

Parameterization in combination with anonymous unions might be 
of use for instance to define error tolerant function composition:

  compose:: ('a -> ('b + error)) * ('b -> ('c + error)) -> 'a -> ('c + error)
  compose(f,g)(x) = if f(x) isa error then f(x) else g(f(x))

The signature of compose will be inferrable again. 

 >Perhaps you don't demand as powerful a type language as I do...
 >(arbitrary type union, intersection, dependent types, higher-order
 >functions)

Well, maybe I'am not so idealistic in respect to the level
of the workaday problems in program developement.

However, probably no one ever worked with higher-order functions 
will dispense with it. So it might become some day with 
dependent types, although its hard to imagine (for me at least, 
currently. printf, *the* example for dependent typing, is not the
function I use all the day ...).

I agree completely with the statement someone else posted recently:
essential, playing with dynamic types opens the mind for recovering 
some more avangardistic programming techniques and inspires the resarch
in typing theory. 

Theory about typing is theory about programming. I wonder if theory
can be build up reasonable from dynamic typing :-?  

--
Wolfgang Grieskamp 
wg@opal.cs.tu-berlin.de tub!tubopal!wg wg%opal@DB0TUI11.BITNET