Type Theory Code

Motivation

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

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'.

There is more information about this SPAD pattern matching mechanism on page here.

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

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

To try the code download 'Interpret.spad' from github and compile it like this:

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

 

 

metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.