[mercury-users] type (class?) parameters

[Richard A. O'Keefe]

I wrote:
	> There's no need to use unary for types.  A good way to represent numbers as
	> sum-of-product types is nat = z | tp1 nat | tp2 nat (0 | 2x+1 | 2x+2) where
	> each natural number has a unique representation.  It works just as well as a
	> type.
	
Michael Day replied:

	I'm afraid I can't quite follow that, particularly tp2 (is that Haskell
	syntax?) What do tp1 and tp2 stand for?
	
No, it's not Haskell syntax.  The stuff after "tp2 nat" is a COMMENT.
It answers the question "what do tp1 and tp2 stand for".

	:- type nat
           ---> zero		% zero represents 0
	      ; tp1(nat)	% tp1(X) represents 2*X'+1 (TwicePlus1)
	      ; tp2(nat)	% tp2(X) represents 2*X'+2 (TwicePlus2)
	      .			% where X represents X'.

To prove that a natural number N has a unique representation in this way:
    If N is zero, can only be represented by zero.
    If N is even and not zero, then N = 2(M+1) for a unique M, so
	can only be represented by tp2(M') where M' represents M,
	and by induction M' is unique.
    If N is odd, then N = (2M)+1 for a unique M, so
	can only be represented by tp1(M') where M' represents M,
	and by induction M' is unique.

There are more obvious representations, but the ones I've looked at do
not have this property, which you need if two numbers-as-types are to
unify when and only when the numbers they represent are the same number.

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------