From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!mx05.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail
From: Jacob Sparre Andersen <jacob.sparre@koparo.com>
Newsgroups: comp.lang.ada
Subject: Weaker typing as a part of the way to stronger typing? (Was: Seeking
 for papers about tagged types vs access to subprograms)
Date: Tue, 14 May 2013 14:46:16 +0200
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <871u99ohk7.fsf_-_@adaheads.sparre-andersen.dk>
References: <op.wv8jh1c1ule2fv@cardamome> <op.wwbvqzkeule2fv@cardamome>
	<op.wwnp2zkrule2fv@cardamome>
	<u3jaslg5kca7.1gk5ds3d4sx2y$.dlg@40tude.net>
	<op.wwnsmtteule2fv@cardamome>
	<17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net>
	<op.wwny5jerule2fv@cardamome>
	<1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net>
	<op.wwn4oak8ule2fv@cardamome>
	<19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net>
	<kmbohm$elb$1@loke.gir.dk> <p0pf97g5w6xg.jhca6ztjwpde$.dlg@40tude.net>
	<op.wwq9s4l6ule2fv@cardamome>
	<1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net>
	<op.wwrefx1pule2fv@cardamome>
	<cps71yzogw24$.7ol98fxcaurj$.dlg@40tude.net>
	<op.wwriky0dule2fv@cardamome>
	<nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net>
	<kmecg6$et4$1@loke.gir.dk>
	<12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net>
	<kmh7d4$up3$1@loke.gir.dk>
NNTP-Posting-Host: 212.27.23.188.bredband.3.dk
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Trace: loke.gir.dk 1368535576 6009 212.27.23.188 (14 May 2013 12:46:16 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Tue, 14 May 2013 12:46:16 +0000 (UTC)
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.2 (gnu/linux)
Cancel-Lock: sha1:8BluXUFFbm1JadDzw1+BFIc2ScU=
Xref: news.eternal-september.org comp.lang.ada:15556
Date: 2013-05-14T14:46:16+02:00
List-Id: <comp.lang.ada>

Randy Brukardt wrote:
> Dmitry A. Kazakov wrote:

[ Nothing whatsoever about access to subprograms. - Please update the
  subject line to match what you are writing about. It makes it much
  easier for everybody to follow you. ]

>> Weak typing is better?
>
> Yes, because we need to move beyond typing to other forms of static
> error detection. Typing is too rigid to do a good job -- you need to
> include statically known information about the contents of variables
> and parameters, which can change from line-to-line in a program.

Considering that SPARK on one level is rather un-typed (all numbers seem
to be equivalent on the constraint error checking level of SPARK), you
may be onto something.  But how would avoid making a monster like Java,
where programmers can use weak types everywhere (except as the main
subprogram).

> I want checking that is *stronger* than what can be provided by
> statically applied types. Trying to get it by extending the type model
> directly is madness, especially as it makes sharing much less
> possible.

Might be right.  But how would you separate operations on the
representation level from operations on the typed ("profile") level?

Greetings,

Jacob
-- 
"... there may be many others,
 but they haven't been discovered"             -- Tom Lehrer