Dependent Types:

Dependent Product / Dependent Function

Pi(A(x)) // A is an arbitrary function (returning a type) a(x) : A(x) // Huh?? x |-> a(x) : Pi(A(x:A))

Elimination/Computation: (x |-> a(x))(y) = a(y) : A(y)

Huh!! So is it really just checking that the type of a thing is the same???

Propositions as Types says that this is a universal quantification (\forall)

Dependent Sum / Dependent Pair

// B is an arbitrary type function // -> Sigma(B(x)) is a type // a : A // b : B(a) // -> (a,b) : Sigma(B(x:A)) Propositions as Types says that this is an existential quantification (\exists) Elimination/Computation: p1((a,b)) = a : A p2((a,b)) = b : B(a)

Workshop

Latest thoughts is that modules can provide our "clean-scoping"

The main problem is how we integrate "type-level" definitions like functions, etc. into the definition of a struct.

All of the madness here implies that these should probably just be separate.

So is this as simple as allowing "associated" comptime objects with a variable? -> Hmm, that's an interesting idea. Seems like it could express a lot of invariants... -> Do we want to have these all keyed by type or is that silly? Is there a more principled technique? -> Would let us handle all "type-level" data, including variables, for instance

  • Wait, this can give us tags for free, can't it? Not quite, due to casting, but we're getting closer...

So T as a type is a representation of data + type-level data that we'd like to be able to manipulate totally separately.

// Woah, this is weirdly logical: struct { x: u32 } : { x: u5 } : StructOps(u32)

// But we need to flatten this: struct { x: T, y: T }

TODO: Think more about whether struct modules really make sense. Why can't we just invent our own datatype? Oh yeah! Because that won't get us associated with the respective methods (Except that it can, right? That's part of the module inputs!)

If I define:

const Complex = struct(T: type) { real: T, imag: T };

the idea is that I can define (in an object-oriented way) trait implementations for Complex

const ComplexMethods = impl ArithmeticOps(Complex(T: type)) { fn multiply(a: T, b: T) { return Complex(T){ .real = multiply(a.real, b.real) - multiply(a.imag, b.imag), .imag = multiply(a.real, b.imag) + multiply(a.imag, b.real), } } etc... }

// And then I can constrain T to be T ++ ArithmeticOps(T)

// So separating methods and representations definitely works. So does combining them as T ++ M (all the time, like Rust's traits, sort of), but it seems more limited since we can't split off M

// TODO: Work out the comparison to Rust's traits // Does Rust go all the way or not? Well, it allows you to have non-abstract (non-module) definitions of the interface // I have a feeling this is something we're going to have to bend on, as much as I don't like it...

// On the other hand, implementations are "naturally" colorful and that's okay // Well, hold up. It's okay that they are colorful to the extent that they specify some of the arguments to their interface, // but we really don't want to give them any powers other than that... // Otherwise, we lose our algebraic dependency tree // So maybe types, but no functions?? Seems inconsistent...

/* morphism [21] or through existential types [15]. How- ever, when all types are passed and may be analyzed (as in λML), the identity of types cannot be hidden and i consequently abstraction is impossible. In contrast, in λR a type can be analyzed only when its representation is available at run time, so abstraction can be achieved simply by not supplying type representations. */ ^ Reminds me of how we clean out our context so that you know whether we parametric in your argument (we are! You passed it in, after all) // Dynamic types are implemented in λR by including a representation of the unknown type, as in ∃α. R(α) × α // So typeid(T) can be a trait in Zig? Neat!

It does seem worth exploring this for understanding, but I'm not sure it needs to be part of our proposal

Abstract Modules

The key idea is to allow modules which enable an "abstract" typing discipline

What about our old friend duck-typing? That's still possible, by allowing methodsets to be attached to objects: interface Default(T: type) { fn }

Extension: Object-associated methodsets

In order to support the object-oriented style of dispatch used in Zig today (including duck-typing), it's necessary to be able to augment a type with a set of methods.

@bind(x, M) // This binds the methodset M to the object x:T, returning an object of type @TypeOf(T) ++ @TypeOf(M)

Hmm, this binds comptime state to a run-time x... So for instance, what does this return:

if (b) { @bind(x, M) } else { x } Okay this can be ruled out by typing, but what about? if (b) { x = @bind(x, M1) } else { x = @bind(x, M2) } // This cannot be allowed (but it is the same problem that we have with, e.g. comptime var right now)

Casting rules:

T ++ M down-casts to T implicitly
M1 ++ M2 down-casts to M1 (or M2) implicitly

For now, we say that T ++ U is not supported where both T and U are struct types or struct+method types.

That's it, really.

A common pattern in many implementations may be to create a factory that returns an struct+method object.

Now we just need a shorthand for creating such an object. This is: @bind(Type{ }, M);

T ++ U, where T and U are both structs (not methodsets) is not allowed
That's it, really

How to translate typical examples to modules

Duck-typing is still allowed, but is not preferred because it's not documenting and doesn't enforce signature correctness.

interface GenericDoubler { fn double_me(x: anytype) // x must be of type T ++ M (where M supports whatever ops are used in the impl of add(T)) }

We can even duck-type the input modules used to build-up a module:

fn U32Doubler(M: anymodule) { return GenericAddOps(u32) { fn double_me(x: anytype) { return M.add(x, x); } } }

For a published module, this would be considered bad style. If the "Struct constructors + implicit constructor constraints" proposal is accepted, that provides a mechanism to achieve the same behavior with better documentation of the intent:

interface GenericDoubler(Integer: type(u32)) { fn double_me(x: Integer(comptime var N)) // x must be of type T ++ M (where M supports whatever ops are used in the impl of add(T)) }

GenericDoubler(Integer); 

// TODO: Referring to type families generically (e.g. a type family indexed by u32) seems strange but is hopefully not too onerous...
	// This is what julia uses bounded types for, right?

We can even duck-type the input modules used to build-up a module:

fn U32Doubler(M: anymodule) { return GenericAddOps(u32) { fn double_me(x: anytype) { return M.add(x, x); } } }

Examples

Okay, so this design would separate interface definition (interface), implementations (impl), and data representation (struct).

Nonetheless, one might reasonably ask, is it worth all this effort? What do we actually get for all this?

The answer is that we get a remarkable level of extensibility.

To demonstrate, here are examples of libraries which are not commonly accomplished in other languages:

Libraries: - Push/pull agnostic stream library (modeled after [?]) - Generic Linear Algebra library, including specialization for small fixed size matrices and custom integer operations for graph-operations - FFT library

In addition to this, there are generic "transforms" that can be applied to programs as well: - Thunked/Memoizing computation transformation - AST generation and interpretation (enabling DSLs) - Automatic differentation (Forward/Reverse/Mixed)

If we support an extension that exposes built-in Zig constructs as their HOAS counter-parts, this can even be used for abstract interpretation: - Stacked borrows, etc.

All of this sounds wild, but it's actually quite explicit and user-controlled.

Not only that, but the concepts can be combined:

Here's a module that performs automatic differentiation on an abstract matrix and then thunks the result:

// Boom bam bim

* On a highly technical note, even comptime itself can be implemented as a set of operations that async might even be the same (being built on top of resume/sleep) -> TODO: demonstrate

interface GenericAddOps(M: anymodule) { fn add(x: anytype) // x must be of type T ++ M (where M supports whatever ops are used in the impl of add(T)) }

interface GenericAddOps(U: type) { // So we can still do object-associated dispatch

fn add(x: comptime var T ++ AddOps(T, U));

// status quo:
fn add(x: anytype) // x must be of type T ++ AddOps(T, U)   (or interface with same "signature")

}

// TODO: Why am I allowed to refer to type/interface types but not modules here?

const Op = impl GenericAddOps(T, u32) { fn add(x: T ++ AddOps(T, u32)) { x.add(5); } } -> This acts like an "infinite" (i.e. functional) version of Op(u8) ++ Op(u16) ++ Op(u32) ... etc. -> The problem here is that I need a "single function" version of the interface and definition

Something like impl GenericAddOps(U).add(x: T ++ AddOps(T, U)) { x.add(5); } or simply: fn add(x: T ++ AddOps(T, u32)) { x.add(5); }

Both of these suck. The second one has no straight-forward abstractification. The first one is ugly and unclear (it implicitly generates an anonymous module impl which is mapped to the function name. Not only that, but it's syntax gets a lot closer to general generics

interface GenericAddOps(U: type) { fn add(x: T ++ AddOps(T, U)); fn add(x: anytype); // This maybe shouldn't be allowed, since it's not documenting at all (but it's equivalent to usual duck-typing) }

// Maybe the right solution for the duck-typing really is some type-inference then. Let's think about this. If I have an M_combined = GenericAddOps(u32) ++ GenericAddOps(u64), then I want to be able to resolve: M.

const Op = impl GenericAddOps(T, u32) { return { fn add(x: T ++ AddOps(T, u32)) { x.add(5); } } } // -> The problem is that the type of this interface is parameterized + and I can't resolve through it. // -> This is almost exactly the "for-all" problem that rust has to solve traits for? // No, this seems more like a case of laziness. The calculation in this case is fine, but the function specification isn't clear about that

const Op = fn(T) {

}

This makes explicit something that's not immediately obvious when programming normally: All computation is built up out of a small set of primitives. Only the compiler/machine ever provides a truly "primitive" operation (such as adding u32).

Okay, so the in-object vtable approach avoids mixing modules because of the fact that a vtable is physically in the object. As long as this isn't swapped out, everything is fine.

Can we do the same thing, but with comptime "ghost" state?

Okay, I got hella distracted with this ghost state stuff. Let's grab some food and come back to all this...

Finish designing our module system (esp. for run-time vs. comptime colorlessness)

// I want this to support Iterator(T), but let's see I want to require it to use one Iterator(T) at a time

// The simplest case is to associate some comptime state with the struct

// When it is used with an interface, that comptime state is updated/checked to verify that the invariants // are preserved (i.e. in this case, it puts a lock on the type)

struct T { x: u32, y: u32, }

// TODO: Encode type closure here struct(T) { ptr: * size(var N: usize) erased T, // Just a pointer to some storage sz: usize };

into() [5]u8 { return @cast(ptr, ).*; } // In this case, the compiler in the debug mode stores "more than necessary" // since it stores its own invariant in combination with ours, since we know we don't want to actually // lose that invariant

// A solution which communicates to the compiler that you want both is: // const Slice = *[var N: usize]u8; // This is a struct function!

// This is a kind of comptime-runtime-agnostic version of weak (parameterized) refinement types // N should be read-only, but copyable

// As usual, we lift a function over the existential // (which I'm sure has some interpretation within first-order logic that will clarify limitations) // In fact, Zig in many cases feels like skolemization!! or herbrandization or predicate functor logic

// Main problem is this: // That invariant should probably not be up to every implementation to enforce on its own // Is there a way that we can re-factor to support this?

// It really is a lot like a lock... and the same "lock" could give us ownership, right? // Seems very plausible... Time to re-visit FCSL again? Perhaps.

// The "brute force" technique just adds an "attribute" to the type (like parent(T)) but in this case // iterator(T) or whatever

// This would give us equivalent protection to the run-time checks, and the same enforcement mechanism // as our solution to the @fieldParentPointer problem. Nice!

// SO: Exploring co-algebras is an important next step for sure.

// Are "attributes" coalgebras?

// For now, let's take the easy solution and just not make it easy to incorrectly replace the usage of an object // inconsistently

// So for now, we postpone this until we can consider more general DT systems

// Another idea: What if you could just test a DT property for some inputs // (this is exactly what tests usually do, actually)