Commit c920b968fdd39829b2391901641954f0f586c86d - Robin

Explain about picking the first semantically equivalent definition. Chris Pressey 5 years ago

2 changed file(s) with 29 addition(s) and 19 deletion(s). Raw diff Collapse all Expand all

-6

HISTORY.md less more

4	4	---------
5	5
6	6	* The meaning of multiple `define`s of the same symbol
7		has changed: it is allowed for the purposes of
8		providing multiple equivalent definitions of a symbol.
9		The implementation is allowed to (but not required to)
10		try to disprove the definitions are equivalent. This
11		obviates the need for `define-if-absent`, which has
	7	has changed: it is allowed for the purposes of providing
	8	multiple semantically equivalent definitions of a symbol.
	9	The implementation is allowed to (but not required to) try
	10	to disprove the definitions are semantically equivalent.
	11	This obviates the need for `define-if-absent`, which has
12	12	been removed.
13	13	* Two macro values are now considered equal if their
14	14	definitions are exactly equal (intensional equality

19	19
20	20	* There are now QuickCheck tests that check whether
21	21	the multiple definitions for a symbol, when given,
22		are equivalent.
	22	are semantically equivalent.
23	23	* `error` is no longer used anywhere in the source.
24	24
25	25	Robin 0.6

+23

-13

doc/Robin.md less more

642	642	? unbound-identifier
643	643
644	644	A name may be defined multiple times. The meaning of this is that
645		several _equivalent definitions_ are being given for the name.
	645	several _semantically equivalent definitions_ are being given for the
	646	name. In this context, "semantically equivalent" means that given the
	647	same arguments in the same environment, the two defintions will always
	648	evaluate to the same value.
646	649
647	650	\| (define true #t)
648	651	\| (define true #t)

650	653	= #t
651	654
652	655	An implementation is allowed to check that the definitions are
653		equivalent, and object with an error condition if it can prove
654		that they are not equivalent. So, for example, the following
655		is allowed to be considered an error:
	656	semantically equivalent, and object with an error condition if it can
	657	prove that they are not semantically equivalent. So, for example, the
	658	following is allowed to be considered an error:
656	659
657	660	(define true #t)
658	661	(define true #f)
659	662
660	663	An implementation should not, however, object with an error condition
661		if it cannot prove the inequivalence (although it is certainly free
662		to produce a warning in this case). A good example of this would
	664	if it cannot prove the semantic inequivalence (although it is certainly
	665	free to produce a warning in this case). A good example of this would
663	666	perhaps be a definition of a function that goes through a Collatz
664	667	sequence and evaluates to `#t`, and a function that simply always
665	668	evaluates to `#t`.
666	669
667	670	An implementation is also allowed to simply take it on faith that
668		the definitions are equivalent. (This is not the best example.)
	671	the definitions are semantically equivalent. (The following example
	672	is perhaps not the best example.)
669	673
670	674	\| (define true #t)
671	675	\| (define true ((macro (self args env) #t)))
672	676	\| (display true)
673	677	= #t
674	678
675		If they are not genuinely equivalent, of course, that is a bug,
676		like any other bug — the semantics of Robin's `define` do not
677		excuse the programmer from exercising their own diligence. The
678		question of which definition Robin picks in this instance is not
679		a sensible question, because the definitions are supposed to
680		be equivalent.
	679	If they are not genuinely equivalent, of course, that is a programmer
	680	error like any programmer error — the semantics of Robin's `define`
	681	do not excuse the programmer from exercising their own diligence.
	682
	683	Since the definitions are supposed to be equivalent, which definition
	684	the implementation chooses, is ultimately up to the implementation.
	685	The implementation could even choose to use different definitions in
	686	different places. However, the current convention is that the
	687	definition that is generally preferred because it is the most efficient
	688	will be given first (perhaps as a built-in provided by the implementation),
	689	so implementations would do well to support choosing the first definition
	690	for each symbol that has multiple definitions.
681	691
682	692	### `reactor` ###
683	693