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!mx02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Haskell, anyone?
Date: Sun, 15 Nov 2015 20:11:17 -0800
Organization: A noiseless patient Spider
Message-ID: <87d1vaoa6y.fsf@nightsong.com>
References: <c6ac0d2f-52af-4aa6-ba6f-34f61e3c93e8@googlegroups.com>
	<dd1ada14-493d-44fc-a081-3a69515f2702@googlegroups.com>
	<n2b23f$aom$1@speranza.aioe.org> <87mvue50ey.fsf@ixod.org>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="811568160cd9f4c22b2423e1fab39dcc";
	logging-data="22124"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+0RCrb6hKSMwek1/+UKcKO"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:dU2kw1Oamn60FuvGgjSXUD74tDc=
	sha1:2SfQe1vbvDh72Ww2GBuOKPDgK8I=
Xref: news.eternal-september.org comp.lang.ada:28387
Date: 2015-11-15T20:11:17-08:00
List-Id: <comp.lang.ada>

Mark Carroll <mtbc@bcs.org> writes:
>> Say define a new integer subtype that can only take values from only
>> 1...20.  And have the compiler and run time check for this?

> I /can't/ think off-hand how to do this easily with Haskell (at least
> without unusual extensions) but I /think/ that Idris, ...

Haskell doesn't have subtypes per se.  You could define a new numeric
type that does a runtime check that a value created in that type is in
range, or throws an error otherwise.  This is called a "smart
constructor" in Haskell.  I think Ada's range types are similar: if X,
Y, and Z are in that 1..20 range type and X=15 and Y=15, then Z:=X+Y is
a legal Ada statement that doesn't raise any error until runtime.
Haskell's concept of types is entirely static (compile time) so Haskell
wouldn't consider "range 1..20" to be a type unles it could verify at
compile that Z:=X+Y was in range, by analyzing the code that produced X
and Y.

There's a new experimental Haskell feature called "refinement types"
which does things like that, and Idris (and Agda and Coq) are built to
do such things, but that's all way beyond what traditional Ada tries to
do.  It's more like SPARK on steroids where there a bunch of proof
obligations ("verification conditions" in SPARK terminology) that have
to be satisfied with almost every statement.

So I'd say don't worry about this til you've gotten more used to the
basics of Haskell.  If you really want to know more, there's another
online book "Software Foundations" that goes into it using Coq:

  http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

Meanwhile there's a Haskell newsgroup comp.lang.haskell which is usually
quiet, but some knowledgeable Haskellers hang out there, so you can get
questions answered there.  The Freenode #haskell IRC channel is also big
and friendly, plus there's the mailing lists, etc.  See www.haskell.org
for more info.