~icefox added T-THOUGHTS 4 years ago

~icefox 4 years ago

Properties of functions to consider: Pure, const (kinda the same as pure probably), no-panics...

~icefox 4 years ago

Related: https://without.boats/blog/the-problem-of-effects/

~icefox 4 years ago*

Okay, here's a WIP list of props that I want to be able to express. Notice we have a list for data and a list for functions...

For data, we have:

• Copy -- Data can be copied with memcpy
• Send -- Data can be sent between threads
• Sync -- Better name maybe; references to data can be sent between threads
• Zero -- Data where zero is a valid default value
• Pod -- Plain ol' data, where any byte sequence is valid. Also consider bytemuck::Contiguous.
• Unpin/Nonpin? -- Data with no internal references; think about this one more.
• Sized? -- Type has a fixed size known at compile time (ie, no variable-length arrays or dyn objects).

For functions, we have:

• Panic -- Function may panic
• Pure -- Function is pure, has no side effects
• Const -- Possibly related to Pure, function can be evaluated at compile time if we try hard enough
• Unsafe -- Function may contain unsafe blocks
• Alloc -- May allocate on the heap (might not be necessary if we make heap allocators always explicit, a la Zig)
• Terminate -- Can be proven to run in a constant time/space (may be useful for realtime stuff)
• Fixed stack -- Does not contain alloca or non-tail-optimizable recursion.

Hm, what else do we need to be able to express?

Not sure whether you have to annotate these explicitly or whether they're just figured out by the compiler. Both have problems.

~araspik 4 years ago

One very cool idea I've found, inspired by this, is of having 'tied types', i.e. types whose each value is tied to some other value. For example, an Index structure may be tied to Vecs, so that every value of type Index is 'tied' to a value of type Vec. This allows not only for compile-time-proven elision of runtime checking, but also for implementing traits!

Consider a structure Sized (which contains size: usize, i.e. the size in bytes) tied to values of type type (i.e. types). You would have an instantiation of Sized for e.g. i32 where size = 4. This neatly provides for run-time and compile-time generics, as if you want information about a type (such as its size), you simply request an instantiation of a tied structure providing that information (i.e. Sized) which is tied to that type. For example:

struct Sized for type { size: usize };
fn alloc(T: type, sized: Sized for T) -> Box<T> {
    // Allocate space of size `sized.size` and return it wrapped in a `Box`
}

Such a function could be inlined at compile-time when the arguments are known, making it essentially just a typesafe malloc, or used at run-time with unknown types with the help of RTTI. It's just very neat, and it can be used to implement all the 'props' you've listed as simple zero-sized types. Also, you could provide multiple traits for different kinds of sizing (compile-time known, which includes the length as a field, run-time known, which includes a function to calculate it, and unknown, which has no extra info). The only reason Sized doesn't provide the length in Rust is because that information is implicitly provided everywhere (e.g. with dyn objects it's stored as an additional field).

There are some unresolved problems with tied types as traits, however: they allow for multiple different instantiations, and so may provide conflicting information (e.g. two different Sized values are constructed for i32 which say size = 4 and size = 2) - this can be overcome with Rust's orphan rules, so that only the module where Sized is defined can construct new values for it; they add some boilerplate in the source code; the compiler would need to track the tied value around to ensure that it still corresponds; and there are complex interactions with (im)mutably borrowing the tied value.

Just some food for thought.

~icefox 4 years ago

Oh wow, that article is utterly amazing. Thank you! It definitely has given me plenty of things to think about, and I need to re-read it again a time or two. I'm still pre-coffee though so I need some more time to absorb it. Two things that stand out to me:

• If we use ZST's for expressing properties of functions, we need syntactic sugar around it. I love the idea and I am very quickly going to get sick of writing stuff like let add: Pure[NoAlloc[Fn(I32, I32): I32]] = .... It also means that adding traits to a function, ie making the restrictions stricter, is an API-breaking change. (If types are expressed in names via mangling or such, it's also an ABI-breaking change.)
• It also looks like it doesn't compose particularly well. What is the difference between Pure[NoAlloc[Fn(I32, I32): I32]] and NoAlloc[Pure[Fn(I32, I32): I32]]? If we proceed only using something like Rust's ZST's then these types are entirely incompatible, and you'll have a lot of functions that do fairly pointless things like juggle X[Y[Z]] -> X[Z]. I can think of times when that would have actual semantic meaning, but also plenty of times where it doesn't. If you get general enough I bet you could start expressing variable-length lists or unordered sets of properties in the type system, but that brings us to the next point...
• If you go far enough in this direction to be really cool you also start getting into advanced type systems such as linear types, which I'd like to avoid if possible. They're complicated, they're hard to implement and they're generally unable to be checked efficiently, as far as I can tell. (...and I don't like reading type theory papers.) Rust and Zig both avoid these sorts of systems for IMO pretty good reasons, so I would like to find a pragmatic subset of these capabilities that give you most of the cool stuff that people will actually commonly use.

So I like that idea a lot, and want to keep thinking about that approach and persuing it. But it's kind of raw as-is. One thing I'd like is for the compiler to infer the properties of a function, so if you really don't care whether println() allocates or not you don't have to say anything about it, but if you really care that your function is NoAlloc then the compiler can prevent you from accidentally calling a function that allocates.

Lots of good food for thought there, thank you.

~araspik 4 years ago

Ooh - we seem to have arrived at a misunderstanding. Consider the following example:

fn foo1(T: type);
fn foo2(T: type, sized: Sized for T);
fn foo3(T: type, sized: Sized for T, pod: POD for T);

While Sized for T is a struct in its own right, it does not represent T (in that it cannot be substituted for T directly in code), but provides additional information. As such, Trait1 for Trait2 for T isn't providing implementations of Trait1 and Trait2 for T, but the much weirder case of the implementation of a trait upon the implementation of a trait upon a type. Traits for each generic type, as required by a function, are passed separately as individual parameters. There's still a lot of boilerplate involved, but there's no ordering issue. There is also (still) the issue of multiple implementations of a single trait for a single type. For some traits (particularly where specialization is concerned), multiple implementations makes perfect sense, and is not really an issue (except that code has to pick a single implementation) - but for traits like Sized, we want a unique implementation. One option is to not regulate it, and to simply state that Bad Things™ will happen if multiple conflicting implementations are created, but this is quite against the spirit of safety of Rust. Another option is to use some sort of special annotation or attribute, and get the compiler to check uniqueness, which I guess can work.

Actually, I just realised that the 'unique implementation' concept may have significance for tied types in general, not just with tied types as traits. I'll need to think about that.

You've hinted at a second issue - negative constraints. This entire system assumes that traits are meant as an opt-in feature, that code can only depend upon a type implementing a trait, not upon a type not implementing a trait. I don't even know where to begin with allowing for them.

Reading about linear typing on Wikipedia, it looks like linear (and affine) typing is simply Rust's ownership and borrowing rules. What do you mean by the term?

I'm happy to provide discussion - I've been aiming at the same space between Rust and C with my own experiments, and so it's really great to see work by the others in this area.

~icefox 3 years ago

Related: https://github.com/fsharp/fslang-suggestions/issues/243

How does F# handle this sort of thing, anyway?

~icefox 3 years ago

A proof-of-concept-ish idea for properties may be to simply allow users to annotate arbitrary properties onto things, and make them "sticky" so that if a function/type has a property, any functions/types that use it will have the same property unless explicitly removed a la Rust's impl !Sync for .... That may or may not be actually useful or at all like what we want in the long run, but may be enough to start playing with ideas and see if it feels good at all.

~icefox 3 years ago*

Between 1ML and other things, I seem to have slowly converged on something resembling ML modules, for the moment. The key question is "what are the fundamental objects the language manipulates"? In Rust there's kinda a lot: there's functions, consts/globals, then also modules, types, traits, probably some other things I'm forgetting. What if there were only values and types? Well then, how do you do modules? Well modules can just be structs that are always evaluated at compile time. This lets you have "associated types", and to some extent generics, that are just first-class types that can be guaranteed to be evaluated at compile time. With that constraint, you can use any normal language construct with them. Functors become plain functions.

This turns out to work, and basically end up being ML modules, which are actually pretty okay but IMO hampered by poor ergonomics from both the "module language" distinction and also the kinda weird specification of scopes/types (a Self type is syntactic sugar but also really useful) and also the kinda weird handling of what is and is not public/transparent. The 1ML paper demonstrates that you don't actually need a separate "module language" for them, just a bit of disambiguation sugar. I'm totally fine with disambiguation sugar in moderation, so I'm just operating based on the idea that it will work out in the end.

The main difference between ML modules and Haskell typeclasses/Rust traits is the latter dispatch based on types, and in the former dispatch is always explicit. As far as I can tell. Apart from that they largely do the same things! Not dispatching on types is honestly a little inconvenient, but isn't a bad basis for a language, so let's roll with it for now and see how it goes. It fits with our current theme of "less sugar, more explicit stuff, fewer magic constructs". Also the explicit nature of ML modules solves Haskell/Rust's "coherence problem" with traits, which is nice.

My gut feeling is still that traits are a major source of complexity in Rust, which is a little frustrating. But my impression from reading obtuse papers is also that if you have generics with typeclasses, or generics with ML modules, both result in basically the same complexity issues. So, oh well. For my goals right now, "complex and explicit" is better than "complex and implicit", so I'll roll with it and see how it works.

~icefox referenced this from #39 2 years ago

~matklad 2 years ago

How is dynamic dispatch dealt with in module-based languages? One cute thing about Rust is that trait is used for both static (type classes) and dynamic (wide pointer with a vtable generated at compile time) polymorphism.

With module systems, the answer I saw was “use a record of closures”, but that doesn’t seem to work in a language with Rust-style ownership: with a record of closures, each closure closes over a copy of state, which isn’t workable if you need uniqueness/exclusivity.

What’s more, closures themselves are sort-of just a special case of dynamic dispatch/existential types. fn(T) -> U closure is just dynamically dispatched (Ctx, fn(Ctx, T) -> U) .

~matklad 2 years ago*

~icefox 2 years ago*

Good question, 'cause I don't actually know the answer. I have been low-key assuming that it will work exactly the same, the module you pass to a function just isn't one that can be inlined away at compile time, so it becomes an explicit vtable argument wherever you need it to be. "Use a record of closures" as you say, but a module is already a record of closures anyway. Well, generally a record of non-closure functions thus far, though they could be closures if you want them to be and if the lifetimes involved work.

const IntEq Eq(I32) = ...
const SomeOtherIntEq Eq(I32) = ...

fn all(T | eq_impl Eq(T), collection T[], item T) Bool = 
    let mut result = true
    for val in collection do
        result &= eq_impl.eq(item, collection)
    end
    result
end

fn choose_eq_impl() Eq[I32] =
    if os_random() then IntEq
    else SomeOtherIntEq
    end
end

fn main() =
    -- Static dispatch, IntEq argument gets inlined away
     let x = all(IntEq, something, 3)
    -- Dynamic dispatch, the compiler can't know which Eq[I32] impl will get called
    -- so it is still passed explicitly
    let y = all(choose_eq_impl(), something, 3)
end

So, basically like that. Whether that's actually what will happen and how it will happen, idk. Whether that's desirable, also idk. I can definitely see it being useful sometimes to be able to tell the programmer whether a module impl is intended to be const or dynamic, which this doesn't really express well.

~matklad 2 years ago

Yeah, the module sort-of give VTable for free, but there’s also type-erasure bit. That is, you want to be polymorphic not only in functions themselves, but in the T.

So something like:

type Draw(@T) = struct
    draw: fn(@T),
end

type Trianlge = …
const DrawTriangle: Draw(Triangle) = …

type Circle = …
const DrawCircle: Draw(Circle) = …

fn draw_mono(T | Draw(T), shape T)
fn draw_dyn(shape ???)

type HoldsAnyDraw = struct
   d: ???
end

~matklad 2 years ago

Ah, I think it's possible to do "explicit type erasure". If Foo(Bar) is a generic type with @T = Bar, we can say that Foo(*) is Foo with some concrete, but unknown type instead of T, which gives the user ability to manually construct wide pointers:

type Draw(@T) = struct
    draw: fn(@T),
end

type Container(@T) = struct
   data: @T
   vtable: Draw(@T)
end

type DynContainer = Container(*)

~icefox 2 years ago

Oof. Yeah type erasure is a toughie that I don't think is terribly possible with Garnet's intended design as it stands. The train of thought is kinda "just make a sum type instead of a thick pointer" -> "sum types can't be extended" -> "figure out a representation for them that can be extended and just make people conform to that repr" -> "that's error prone enough it's worth adding special language support for".

Explicit type erasure isn't a terrible place to start, sounds like it would be possible to bolt on with minimal extra complexity. I wonder if one could make it generic somehow such that you don't need to write a separate Container type for every module type? That might start getting very HKT-ish, but you could take it the other way and simply have a macro that generates the boilerplate code for you. That might be a good incentive to start thinking more seriously about macros.

~icefox 2 years ago

So if you try to write it right now the "erase" operation might look something like this:

-- Can't mention @T in the signature here, which is currently invalid but is where the 
-- type erasure has to happens
-- Also these types have to be pointers so that Dyn is fixed size I guess
type Dyn(@Module) = struct
    data: @T^
    vtable: @Module(@T)^  -- Ok  I think that's HKT right there
end

type Draw(@T) = struct
    draw: fn(@T),
end

type Trianlge = …
const DrawTriangle: Draw(Triangle) = …

type Circle = …
const DrawCircle: Draw(Circle) = …

fn draw_mono(T | Draw(T), shape T)
fn draw_dyn(shape Dyn(Draw))

type HoldsAnyDraw = struct
   d: Dyn(Draw)
end

const SomeTriangle: DynDraw = DynDraw {
    .data = my_triangle,
    .vtable = DrawTriangle,
}

const SomeCircle: DynDraw = DynDraw {
    .data = my_circle,
    .vtable = DrawCircle,
}

Yeeeeeeah, not super appealing. Very much something some lang features or macros would want to smooth over. It wouldn't even be particularly difficult to implement, just difficult to reason about in the ML-y type system. When it gets down to the metal, it's a pair of pointers.

~matklad 1 year, 9 months ago*

This is super half-baked, but one thing I realized about Zig recently is that it really just computes types. That is, type system usually have some sort of computational engine embedded into them, but Zig just makes that explicit. See, in particular, https://matklad.github.io/2023/08/09/types-and-zig.html#Mandatory-Function-Signatures .

Now, the trait/module systems usually have some sort of prologue embedded into them, which allows computing of instances. That is, when, in Rust, you write impl<T: MyTrait> MyTrait for MyType<T>, that actually defines a type-level function mapping impls to impls, and then there's a smart trait solver which figures out that, if you need MyType<Foo>: MyTrait, you could construct that instance from that function and Foo: MyTrait. The same "implicit computation" idea is present in that modular implicits paper --- complier can synthsize new modules from functors.

Which makes me think that perhaps Zig's approach of "let's use explicit first-order language for type-level computation" can be applied to a problem of searching instances?

Or, more concretely, Zig with default arguments I think could be equivalent to modular implicits? Here's some made-up syntax:

fn sort(
  comptime T: type,
   xs: T[],
   // The trick: we provide default value for `cmp`, which also depends on the previous parameter (`T`)
   cmp: fn(T, T): Ordering = T.cmp,
)

struct Vec<T> {
    fn cmp(lhs: Self, rhs: Self,  cmp: fn(T, T): Ordering = T.cmp) 
}

We can then call sort(Vec<Int>, xs), and that'll use Vec<Int>.cmp for sort's cmp default. And Vec<Int>.cmp would use Int.cmp for its default.

That is, we get ourselves type-level "implicit search & construction of derived impls" behavior via seemingly much more tame runtime-level default arguments for functions.

~icefox 1 year, 9 months ago*

Hmmm, interesting observation. Thanks for linking me that article, it's a pretty interesting summary in general...

The trick: we provide default value for cmp, which also depends on the previous parameter (T)

This is quite interesting because that's more or less how you do things with modules already, you can specify an operation in terms of another module you have... It sounds like what you're doing in your case is attaching a default instance to a particular type. Contrast with modular implicits where the default instance is based on the values that are currently in scope, I think? How would you implement an Ordering module for a new concrete type, in your made-up syntax?

---

Semi-related, I think, is that I think I've finally figured out the fundamental difference between generics a la Rust, OCaml, Haskell etc, and templates a la D, C++, arguably Zig, etc. Generics work by checking the types, and then generating the code for them. Template systems do the opposite: they generate code and substitute in the types, then typecheck what they've generated. Basically macros, optimized for dealing with types. I am a little torn sometimes about using generics for Garnet, because templates are actually very nice and pragmatic and results in a simpler type checker. They just have some nasty properties when they fail, and their type-level programming is more ad-hoc (but also potentially more powerful because of it). But... eeeh, there need to be more languages out there with ML-y modules, so let's keep doing that.

~matklad 1 year, 9 months ago

Generics work by checking the types, and then generating the code for them. Template systems do the opposite:

Yeah, that's the thing, one is a proper type system (if the signature works, the body can't break), another is a glorified macro. What I am getting at here is another distinction between Zig and others, which is orthogonal.

In function signatures, there are constructs like Vec<i32> or (in Zig) ArrayList(i32). Usually, those are "programs" in some obscure logical language, but Zig makes them into you usual imperative language. In Rust, Vec<i32> and Vec<i32> are equal types, because those are equivalent terms. In Zig, ArrayList(i32) and ArrayList(i32) literally denote the exact same value, because comptime computations are always interned.

So,

It sounds like what you're doing in your case is attaching a default instance to a particular type. Contrast with modular implicits where the default instance is based on the values that are currently in scope, I think?

is exactly it! With modular implicits, compiler synthesizes the required instance looking at what's in scope. What I am proposing here is to make this "instance synthesis" a very dumb computation in the hands of the programmer. In a way, that's a Zig way to do modular implicits.

How would you implement an Ordering module for a new concrete type, in your made-up syntax?

So here, the "module" is just fn cmp(T, T): Ordering. That is, just a function, not really grouped into mod Ord { fn cmp }. And the way it works, you can declare fn cmp inside the type you are writing:

struct IntPair {
    x: Int,
    y: Int,

    fn cmp(lhs: IntPair, rhs: IntPair): Ordering { /* compare x & y */ }
}

This allows plugging Vec<IntPair> into sort such that compiler figures out (synthesizes) the code for comparing vectors of points. Note that this blesses this particular semantics of cmp. If I want to add a non-standard instance (like comparing points only by X coordinate), I write this as a top-level function:

fn cmp_by_x(lhs: IntPair, rhs: IntPair): Ordering { ... }

fn example(xs: Vec<IntPair>) {
  sort(xs); // uses default ordering
  sort(xs, cmp = |lhs, rhs| lhs.cmp(rhs)); // above elaborated
  sort(xs, cmp = |lhs_vec, rhs_vec| lhs_vec.cmp(rhs_vec, cmp = |lhs_pair, rhs_pair| lhs_pair.cmp(rhs_pair))); // above elaborated more

  sort(xs, cmp: |lhs, rhs| lhs.cmp(rhs, cmp = cmp_by_x)) // uses non-standard ordering
}

The heavy lifting is done by

cmp: fn(T, T): Ordering = T.cmp

in the original declaraion. It says "whatever T at the call-site is, lookup a T declaration with name "cmp"" . This of course can fail, if T doesn't have a cmp, and that would be a compile-time error. With modular implicits, the equivalent says something like "whatever the T is, lookup something with fn(T, T) type and available as an implicit at the call-site". The difference is that the latter behavior is fully implicit and hard-coded into the compiler, while the former is the literal = T.cmp written by the programmer at the declaration site.

~icefox 1 year, 9 months ago*

Yeah, that's the thing, one is a proper type system, another is a glorified macro.

Now now, be nice. :-P I've been working on a side-project in Elixir lately and the whole language is a glorified macro. It works remarkably well, and the best measure of quality is "it works". (Also sorry for not getting back to this for a week because of that.)

because comptime computations are always interned.

ah-HA, this is an important distinction that I didn't know, and which I think solves a problem I've been avoiding thinking about. Basically the nuisance of explicit instantiation of modules, where you have to say const IntList = List.new(Int) or such. The question is, if you have multiple instances of that, how do you prove they're equal so that a) you can have two IntList decls in two different files and the compiler knows they're actually the same thing, and b) you can dedupe the code generated for it and not have multiple copies of the same instantiation around. I've been mentally brushing it off as "the compiler can figure out they're actually the same, it's ok" but have been putting off figuring out exactly how that would look/work. "comptime computations are always interned" is a very good summary of it...

...though it then makes me wonder about separate compilation issues, since it seems like you then need a cache of comptime computations that any compilation unit can read/modify. And that has to be part of the ABI, so you can have two object files that are compiled at separate times but are still linkable. So the interned computation has to get put into the .api file or such? Not insurmountable, but kinda weird.

uh let me try to get my brain back onto your actual point...

In general I like the idea of using explicit first-order language for type resolution, and kinda slowly been trying to edge in that direction for Garnet without quite going whole-hog and making the entire language run at compile time like Zig kinda does. Might be time to give up on on the doubts and just go for it, see what it looks like, and then see if we can nibble away enough special cases to make the error messages comprehensible. Though that also means having the compiler for the language include an interpreter, or going through a bunch of headache to compile and run the comptime code.

struct IntPair {
    x: Int,
    y: Int,

    fn cmp(lhs: IntPair, rhs: IntPair): Ordering { /* compare x & y */ }
}

I'm immediately suspicious of putting the function into the actual struct, even if only syntactically. I guess your example lets you specify them explicitly, but it feels like it couples "what modules this type implements" to "what the original writer thought of at the time"... which is what Rust traits do. Part of the point of using modules is to decouple that, to remove the coupling of definition and instance. On the other hand it might be suitable for a shortcut, and it sounds like the whole point of this is to make it easier to shortcut the common cases without otherwise changing semantics? ...I'm probably overthinking this. Having a blessed default is useful a lot of the time.

So I wonder what happens when this gets more complicated? What if cmp() is something that has a generic type parameter? Then I suppose it would have to be a type parameter that otherwise exists in the enclosing type, so you could have Pair<T> { ... fn some_op(arg: T, ...) } but maybe some_op() wouldn't be allowed to introduce its own type params? Or maybe it can, but that starts feeling like you're doing partial-evaluation of your comptime functions and that makes my head hurt... Though we're kinda doing this already.

I need to get a good night's sleep and come back to this, I think.

~matklad 1 year, 9 months ago

ah-HA, this is an important distinction

Note that both Zig and C++ work that way --- if you write recursive comptime/template fibonacci, compiler will evaluate it in linear time.

...though it then makes me wonder about separate compilation issues

Both Rust and C++ use ODR here --- each compilation unit gets a separate, fresh copy of "unique stuff computed at comptime", and then its up to the linker to prune away duplicates. Zig just doesn't do separate compilation. I was at first shocked at that, but now that makes sense --- everything you can do with separate compilation, you can do inside a single multi-threaded process, but better, with the exception of two things:

• your program must fit in ram. Original motivation for separate compilation was that programs were too big. These days, we have plenty of RAM. What's more, the most RAM-hungry bit, linking (with lto) is not separate anyway.
• build must be local, no distributed builds. This seems like a bigger issue --- with separate compilation, you might scale beyond a single machine, but with threads and shared address space, you can't use more CPUs than you have. OTOH, if your compiler isn't slow, you can compile a boatload of code on a single computer anyway.

~nicolterra 1 year, 8 months ago*

Hey, I am new here. I am Nicol. I am just a tinkerer and new-ish programmer. I wanted to make my own Garnet programming language for games, actually. I found your project on a chance google search. So embarassingly, I am changing names LOL. THANKS FOR THAT

Other then that, I love the idea. I am considering something deeper, but I love type meta programming.

PS: I would clone, but since I have my own language so obviously just as busy, I just came to tell you this. My language will aim to be a VM that can bootstrap other compilers/interpreters to it for transpilation. Using Nim, and a certain popular go book as a base.

~icefox 1 year, 8 months ago

Hi Nicol, sorry for the late reply! Nice to meet you. I was actually pretty surprised not to find an existing language called Garnet when I started this, so I knew I had to grab it quick before someone else did. ;-) I have a long list of other good rock/mineral names somewhere if you want suggestions though!

Glad you like the language though, or at least the ideas around it. I... kinda hate type metaprogramming honestly, but it's just so damn useful!

Having a VM for bootstrapping honestly sounds like a nice feature; my intention was always to just use webassembly for that purpose. Have the compiler able to output wasm, and then it can bootstrap on any system with even a basic wasm interpreter. I tried this early on for garnetc and it worked well but I haven't really touched the idea in ages.

Maybe I should actually use the mailing list for something, or have some other useful communication medium... 🤔

~icefox referenced this from #36 4 months ago