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.

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

Concrete

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

Category

A concrete type may be an instance of a category. A category may provide information about the concrete type.

Possible Category Data

• Methods (interface)
• Fields
• Call-able