[m-dev.] :- type (type).

[Mark Brown]

Hi,

While coding (and debugging!) my kind inference pass, I've come across
numerous pieces of code with the following pattern:

    ( type_to_ctor_and_args(Type, TypeCtor, Args) ->
        TypeCtor = SymName - _Arity,
        (
            type_ctor_is_higher_order(TypeCtor, _, _, _)
        ->
		...
        ;
            type_ctor_is_tuple(TypeCtor)
        ->
		...
        ;
            ( SymName = unqualified("int")
            ; SymName = unqualified("float")
            ; SymName = unqualified("string")
            ; SymName = unqualified("character")
            )
        ->
		...
        ;
		...
        ),
        ...
    )

A significant problem that I've been having is that the compiler can't
help me to find constructs of this sort and check whether they need to
handle kind annotations or apply/N expressions specially.

I am therefore going to propose that we move away from the types-as-terms
representation and design a type that is specifically for Mercury type
expressions.  I think this is what we would eventually be doing anyway,
and doing it before I complete the kind inference will help immensely.
Before I proceed though, I'd like to request that the basic data structure
be reviewed first, since changing them later will be a lot of tedious work.

So here's the main types I propose to (re)define.

:- type (type)
	--->	variable(tvar, kind)
			% A type variable.

	;	defined(sym_name, list(type), kind)
			% A user defined type constructor.

	;	builtin(builtin_type)
			% These are all known to have kind `star'.

	% The above three functors should be kept as the first three, since
	% they will be the most commonly used and therefore we want them to
	% get the primary tags on an x86.  (I believe this is the right way
	% to achieve that.)

	;	pred_type(list(type))
			% A type for higher-order pred values.  The kind is
			% always `star'.

	;	func_type(list(type), (type))
			% A type for higher_order func values.  The second
			% argument is the result type.  The kind is always
			% `star'.

	;	tuple(list(type), kind)
			% Tuple types.

	;	apply_n(tvar, list(type), kind)
			% An apply/N expression.  `apply_n(T, [T1, ...], K)'
			% would be the representation of type `T(T1, ...)'
			% with kind K.  The list must be non-empty.

	;	kinded((type), kind).
			% A type expression with an explicit kind annotation.
			% (This functor won't be added until later.)

:- type builtin_type
	--->	int
	;	float
	;	string
	;	character.

	% Note that at first all kinds will be just `star'.
:- type kind
	--->	star
	;	arrow(kind, kind)
	;	variable(kvar).

Possibly there could also be a change to the definition of the type
`type_ctor', but I'll decide that later.

Some variations that might be considered:

	- Give a kind for every type:

		:- type (type) == pair(type_expr, kind).

	  and leave the kind argument out of the individual functors.  This
	  would give a simpler structure, but would probably be slightly
	  less efficient (and would contain redundant data in the case that
	  the kind must be `star').

	- Allow arbitrary type expressions as the first argument to apply_n/3.
	  This would more closely reflect what appears in the source code
	  being compiled, but would require a slightly more complicated
	  unification algorithm (or would require us to put all types into
	  a canonical form at some stage).

	- Change the type name to `mtype' or something else that is not
	  defined as an operator.  This seems to be the popular choice in
	  the Mercury office but I prefer sticking with `type'.

Any comments?

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------