Type Theory

Hyper-Consistent

I'm really drawn to this. There are a lot of very similar structures in a program that could be brought in line. Although I'm afraid doing this is going to recreate lisp. This also ties into the data spec I'm working on.

The two fundamental container types are an ordered list and an associative array. In a strongly typed context an ordered list is either typed or tuple and fixed or variable length. A variable length tuple just means the last argument is variadic.

But an associative array can be constructed either from two lists zipped together or from a list of key/values. This means that something like a struct is an ordered associative array.

This becomes interesting because the arguments to a function and a struct definition are essentially the same thing.

 definition func(rID receiverType) Name <tupleDef> returnType {...}

And a code block is a list of type Statement.

TypeSet

A TypeSet is an abstract type that can answer

• Does type X belong to typeset T
• What methods are available on typeset T

Interfaces and Tagged Unions are both typesets. I may make typesets the base thing in the compiler and move interface and union out to the standard library. Actually, unions may not be a typeset. They are if I want the implicit interface, but not if they're just a bucket for casting. Then they're an enum and an unsafe pointer in a struct.

After looking at Jai, I'm starting to think something that can express this programmatically would be best. I think the way to do this is programatically build a mapping. So the returned typeset will be a type that acts as a table to the underlying type. I could stick with the interface logic and only do a method table. This also lets me do some of the things I want without drastically complicating things. For instance, it solves the graph node problem that

 func(tn TreeNode) Child(i int) TreeNode
 func(tn TreeNode) Children() int
 
 type GraphNode interface{
   Children() int
   Child(i int) GraphNode
 }

With this sort of logic, we can explicitly cast TreeNode to GraphNode.

Another good case is

 func(f *Foo) Bar(s string, v ...int) float64
 interface {
   Bar(string) float64
 }

The method doesn't fulfill the interface, but it can with no coercion.

And these

 func (s Str) String() string
 func(f *Foo) Up(s Stringer)
 func(f *Foo) Down() Str
 interface {
   Up(Str)
   Down() Stringer
 }

We can again use Foo with no coercion. In Up, we're going to be passing an Str in, but anything that can accept Stringer can accept Str because it fulfills Stringer. And in Down we return a Stringer but returning Str works because Str fulfills Stringer.

Type Type (reflection)

Can type be passed around? This is a good way to do reflection. It would probably be limited to libraries.

Tuple Equivalence

I like using structs everywhere (like func calls). But for Interfaces this creates an issue that we need tuple equivalence.

 <{a,b : int}> --> (int){ <-- a+b }
 <{x,y : int}> --> (int){ <-- x*y }

These should be equivalent types, but the struct field names are different. Doing a tuple compare implies that the order is important, which I don't want. This can be solved with an array

 <[2]int> --> (int){$[0]+$[1]}
 <[2]int> --> (int){$[0]*$[1]}

This does create the need for a "this" symbol ($ in the above) but that may be useful anyway.

Target

Types will be the first thing I do with Gryphon. I will be writing serialization logic using this in other languages before I start working on Gryphon.

Base Types

• Nil
• int
• float
• bool
• string
• struct
• union
• interface?
• typeset?

When thinking about this from a serialization perspective, interfaces get weird because they are based around methods and static data has no methods.

Elegant Nil Check

 if a!=nil && a.b != nil && a.b.c != nil{...}

Lets say these have types Union<A,Nil>, Union<B,Nil> and Union<C,Nil>, we can allow the . operator on Nil to always return Nil. So this doesn't error instead it becomes

 c := a.b.c
 if c.(Nil){...}

There is a complication that if B Union<B1,B2,Nil> where B1 has C but B2 does not, there is a complication.

3 Layer Model

Memory Block

An array of bytes. Has a length and starting address. Can access any byte by index

A block could also have the access level 1) Can modify 2) Cannot modify 3) Static

Concrete

Built on a memory block. Could be a simple type like an int or a more complex type like a struct.

TypeSet

A concrete type may be an instance of a member of a TypeSet.

Possible TypeSet Data

• Methods (interface)
• Fields
• Call-able

Static Type Properties

A Type can have properties (like a class property in Python) but they must be static. Methods are functions on the class that take an instance as the first argument.

A nice detail that falls out of this. There is a Nil type, defining a new type from Nil creates a namespace because an instance cannot be created.

 type HttpStatus nil
 
 HttpStatus.Ok = 200
 HttpStatus.NotFound = 401
 HttpStatus.ServerError = 500

Though this is kind of a bad example because it would be better served by an enum (though maybe this how we do enums).