# Type Theory Code

### Motivation

I am working on a domain to represent types. There are a number of potential applications for this:

• I am working on a SPAD based interpreter (as explained here) and there is a need to represent types in this (see type matcher)
• I also need to represent types in computation related domains such as λ-calculus and combinators (as explained here). It would be good to upgrade the very simplistic representation of types that exists there at the moment.

In order to use the SPAD Rewrite rules and pattern matching capabilities (as explained here) we need to make this domain a ring.

As shown in the table (right) there is a potential correspondence between type constructs and ring operations:

I suspect that, from a theoretical point of view, we want the type system to implement a Closed Cartesian Category (CCC) but due to the practical issue above it might be best to make it a ring for now.

Type Ring
UNION(A,B) A+B
RECORD(A,B) A*B
NONE 0
ANY 1
A->B BA
? -A

On issue with the table above is that I can't see a meaning in a type which corresponds to a minus operation. However, I see no reason why we cant implement minus even though it does not correspond to any actual types.

Also, I'm not sure about exponent to represent function types. For instance: A point in3D space might be represented by Float3, however its hard to see this as 3->Float except in a very theoretical sense.

This is a sort of 'lifting', that is, values in this domain represent types.

### Type Expressions

Because this is a ring (also needs to inherit a few other categories) then Axiom/FriCAS allows us to define expressions over it. This gives the possibility of having variables that represent types and to use SPAD rewrite rules to express type identities, for instance, we might define simplification rules for types like these:

Rewrite rules:
 UNION(x,NONE) == x RECORD(x,ANY) == x RECORD(x,NONE) == NONE RECORD(UNION(x,y),UNION(x,z)) == UNION(x,RECORD(y,z))

There is a problem with this, so far, it is not clear what should be a type constant and what needs to be in an expression. In the above rules, I have used a convention that lower case letters are variables which can be replaced by any types. Its not as simple as numbers where operations on the numbers just produce another number, here operations on types produce a tree structure:

Integer * Float = Record(Integer,Float)

Although the above is a tree structure, I would say that it is still a 'Type' and not a 'TypeExpression' because it does not contain any variables.

### MType

MType is a domain I have written which stands for 'matchable type'. The intention is to be able to represent types in a way that is more powerful than the existing FriCAS types.

I want to be able to have type variables and to use type constructors in a more flexible way.

The original reason for writing this is that I needed to represent types in a SPAD version of the interpreter that I am working on (see page here). In this interpreter it is used by TypeMatcher to hold type information.

We then need to pattern match this. There is a mechanism in SPAD for pattern matching, in ordinary expressions, which is used in specifying rewrite rules. Is there an way that we can use that mechanism, not for an expression on ordinary functions, but for a 'type expression'? that is an expression where all the 'values' are 'types'.

I have therefore written a domain 'MatchableType' which implements:

• ConvertibleTo(Pattern(MatchableType))
• PatternMatchable(MatchableType)

The code I have written to experiment with these things is on github here.

Note: we need to compile first in 'bootStrapMode' and then again normally, this is because the code has circular references.

Now we have compiled it we can run it like this:

 ```)boot \$bootStrapMode := true )co axiom/interpret/types )boot \$bootStrapMode := false )co axiom/interpret/types```
 ```(1) -> A := typeConstruct("A"::Symbol) (1) A Type: MType (2) -> B := typeConstruct("B"::Symbol) (2) B Type: MType (3) -> A + B (3) UNION(A,B) Type: MType (4) -> A*B (4) RECORD(A,B) Type: MType (5) -> 0\$MType (5) NONE Type: MType (6) -> 1\$MType (6) ANY Type: MType```

Is there a way to use it in a rule?

 ```(1) -> RR := testRule() MTypeExpression convert to pattern MTypeExpression convert to pattern MTypeExpression convert to pattern MTypeExpression not MType MTypeExpression not MType (1) Integer == Float Type: RewriteRule(MType,MType,MTypeExpression(MType)) (2) -> EX := testExpression() MTypeExpression not MType (2) Integer Type: MTypeExpression(MType) (3) -> EX := testApply(RR,EX) MTypeExpression patternMatch pat= Type(Type + Type) MTypeExpression patternMatch res= [] MTypeExpression patternMatch pat= Type(Type + Type) MTypeExpression patternMatch res= [] MTypeExpression not MType (3) ANY Float Type: MTypeExpression(MType) (4) -> ```

 ```)abbrev package TESTR TestRule ++ Author: Martin Baker ++ Date Created: April 2014 ++ Date Last Updated: April 2014 ++ Description: ++ I can't work out how to do this from the interprester ++ so I have compiled the test here. TestRule() : Target == Implementation where Target ==> with testRule:() -> RewriteRule(MType,MType,MTypeExpression(MType)) testExpression:() -> MTypeExpression(MType) testApply:(RewriteRule(MType,MType,MTypeExpression(MType)),_ MTypeExpression(MType)) -> MTypeExpression(MType) Implementation ==> add import MType import Pattern(MType) import PatternMatchable(MType) import PatternMatchResult(MType,PatternMatchable(MType)) import MTypeExpression(MType) -- test testRule(): RewriteRule(MType,MType,MTypeExpression(MType))== a1:MType := typeConstruct("Integer"::Symbol) a:=a1::MTypeExpression(MType) b1:MType := typeConstruct("Float"::Symbol) b:=b1::MTypeExpression(MType) rule(a,b)\$RewriteRule(MType,MType,MTypeExpression(MType)) testExpression():MTypeExpression(MType)== a1:MType := typeConstruct("Integer"::Symbol) a1::MTypeExpression(MType) testApply(rr:RewriteRule(MType,MType,MTypeExpression(MType)),_ ex:MTypeExpression(MType)): MTypeExpression(MType)== applyRules([rr],ex)\$ApplyRules(MType,MType,MTypeExpression(MType)) @ ```

 ```(7) -> R1:RewriteRule(MType,MType,Expression(MType)) := rule a+0 == a RewriteRule(MType,MType,Expression(MType)) is not a valid type. (7) -> R1:RewriteRule(MType,MType,MTypeExpression(MType)) := rule a+0 == a There are 1 exposed and 0 unexposed library operations named rule having 2 argument(s) but none was determined to be applicable. Use HyperDoc Browse, or issue )display op rule to learn more about the available operations. Perhaps package-calling the operation or using coercions on the arguments will allow you to apply the operation. Cannot find a definition or applicable library operation named rule with argument type(s) Polynomial(Integer) Variable(a) Perhaps you should use "@" to indicate the required return type, or "\$" to specify which version of the function you need. (7) -> RR := RewriteRule(MType,MType,MTypeExpression(MType)) (7) RewriteRule(MType,MType,MTypeExpression(MType)) Type: Type (8) -> R2:RewriteRule(Integer,Integer,Expression(Integer)) := rule a+1 == a (8) a + 1 == a Type: RewriteRule(Integer,Integer,Expression(Integer)) (9) -> ```