[mercury-users] Square types

[Ralph Becket]

> From: Michael Day [mailto:mikeday at corplink.com.au]
> Sent: 13 June 2001 09:46
> 
> Goodness me, that's clever.

Flattery will get you nowhere!

> One more question. As I can't make an arbitrarily sized tuple an
instance
> of a type class in Mercury, it is convenient sometimes to define a
tuple
> type, basically a list but with the length encoded in the type:
> 
> :- type empty_tuple ---> empty_tuple.
> :- type tuple(S, T) ---> tuple(S, T).
> 
> X = tuple(1, tuple("foo", empty_tuple))
> 
> equivalent to X = {1, "foo"}, but allowing this:
> 
> :- instance something(tuple(S, T)) <= something(T) ...
> 
> Anyway, would it be possible to make a tuple whose length is embedded
in
> its type and can contain only a square number of elements?

A square type instance

:- type square(T) == sq(T, T).

where

:- type sq(N, T)
    --->    zero
    ;       sq(N, sq({T, T, N}, T)).

does contain (the square root of) its size in the number of 
levels of sq/2 nesting.  For example, the 9-square is

sq(_1, sq({_2, _3, _4}, sq({_5, _6, _7, _8, _9}, zero)))

> (To be honest, I'd like to use them to store square matrices of
arbitrary
> size and be able to know that two different tuples have the *same*
size).

Well, you could use type reflection to check that two matrices were the
same size by comparing their types with std_util__type_of/1.  But the
real problem with this approach is that you'd also have to use
reflection to manipulate these structures.  For example, a function that
manipulated square(float) values would have to deal with objects of type
float, {float, float, float}, {float, float, float, float, float} and so
forth.  As far as I know, reflection is the only way to do this in a
type system like Mercury's.

If I were tackling your problem (square matrices) I'd be inclined to
use an ADT whose implementation was something like array(array(float))
which just preserved the invariant that such things were always
square.

- Ralph
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------