Basic type system

[RobertBendun]

Program is compile time evaluated. Evaluation starts with empty type stack. All operations consume and/or produce values and place their types onto type stack. Illegal are:

• ending program with types on type stack.
• trying to pop value from empty type stack
• violating rules for control flow
• mismatching types from required by operations

Operations can have different meaning and result according to types that are on stack. Stack manipulation operations (like drop or swap are supported by all operations).

Types

Type system should support following types:

• bool (result of comparison operations)
• u64 (integer literals, syscall result)
• ptr (string literals, memory declarations, address of function)

Casting syntax is as(bool), as(ptr) ...

Control flow

if blocks

Value consumed by if for determining which branch to execute known as condition should be bool.

• with else data stack types must match on both ends. typeof(then_branch) == typeof(else_branch). Condition and it's type is consumed
• without else data stack must match stack before if with condition value consumed. For program <code> <condition> if <then_branch> end must hold typeof(code) == typeof(then_branch)

while blocks

Stack after consuming condition in do should match this before while. Stack after loop body execution should match this before while.

functions

On each return (including function end) state of stack should be the same. if return is embeded into while or if, it should change behaviour of given block checking.

• When in if branch with return do not have to produce the same stack as other branch or code before.
• When in while stack don't have to match stack before while

Operations and their types

Operations on u64

Basically almost all. Excluded are:

• or, and, call
• store and load only accepts ptr as address
• do and if requires bool as conditions

Operations on ptr

• ptr - ptr -> u64 - (assumes first ptr is the bigger one, otherwise we are in trouble)
• ptr - u64 -> ptr
• ptr + u64 -> ptr and u64 + ptr -> ptr
• equality with ptr and u64
• casting to bool meaning ptr 0 !=
• ptr load<n> -> u64
• u64 ptr store<n> -> void
• syscall<n> should support ptr for it's data arguments (function wrappers will provide stronger typing for syscalls in the future)
• ptr call -> ? - such type system cannot express result of call

Related

Different size and "signedness" of types: #46 Function type specification: #47