is there any language like Rust, with a similar notion of lifetimes and references, and deterministic memory management?

@sodiboo i don't really know it at all, but _possibly_ ObjC/Swift ARC?

it's not really the same, and this space is generally _quite_ sparse

@r Swift has a lot of similarities with Rust and definitely does deterministic memory management, but it does NOT have the primary trait i was asking about: “lifetimes and references”. Swift does not at all support any notion of borrowing like Rust. To pass a “reference” into a function, it will have to be an owned reference counted handle, which is fine for most programs but definitely not at all the same thing as what Rust generally does.

@sodiboo ats, kinda?
you have linear types rather than affine types (stuff has to be consumed exaxtly once, rather than at most once, meaning you can have eg two different drop-like functions and the compiler ensures that you call one of them in all possible paths) and have explicit proofs for stuff (for example "there is memory at this address" and "this memory has been initialized"; they behave a bit like zero size types and are often used similarly to state types in rust)

@buffet hm. that sounds like not what i asked for BUT those are some very interesting properties and i haven’t heard of this before! I’ll check it out some more. that sounds like a nice way to program, perhaps

@sodiboo main differences:
compiles to C and especially for lower level stuff relies on having at least some C that you wrap properly, and is over all more focused on the embedded proof assistant, which gives a lot of flexibility

also a pain in the ass to use, especially if you're trying to read one of the error messages
also "viewt@ype" as a linear viewtype, because that's obviously where the @ goes

@buffet follow-up question: what are some neat languages with linear types?

@sodiboo in general the stdlib has a bunch of crazy naming conventions that never get explained (this is more or less just some profs pet project, even though ats3 is ready for enterprise by definition (too lazy to find the quote))

@sodiboo i've no idea^^
definitely not ats

@sodiboo i think that is what you asked for

rust memory management is a combination of:
- affine types (let x = y; invalidates y), ats does this with the "used at most once" part of linear types' "exactly once"
- raii (aka drop) allowing you to make sure some code gets called on every code path, allowing stuff like reliable Rc, ats does this with the "at least once" part of linear types
- not allowing anyone else to borrow when there's a &mut, ats does this with weird proofs that no one else...

@sodiboo hit the character limit exactly where it was clear what i was saying anyways, so i won't finish my sentence

@sodiboo maybe English or Spanish

@Bosspaint hm. pronouns and other forms of indirect address do exist in a lot of natural languages. i can easily refer to a previous subject in a shorter way, and arguably, that is a “reference” with a “lifetime” because after a certain point, it is no longer valid and any competent speaker will generally “reborrow” the subject by naming it again.

but i don’t think this at all satisfies the requirement of “deterministic memory management”. because, obviously, there are no fixed rules to exactly when and how this works or doesn’t.
and, there is not exactly a compiler or linter that can catch mistakes before you say them. so, it’s as useful as saying that “yeah ! C has lifetimes and references ! you can’t reference a variable after it’s been freed, that’s Undefined Behaviour”. obviously, i mean a language where the compiler enforces these kinds of constraints authoritatively. natural languages are disqualified on that requirement alone. (and no, Académie Française does not count as a compiler, no matter how authoritative they want to be about French)

@sodiboo you made me look at ats code again
and i'm surprised i somehow was once able to understand what's going on
my instance does not give me the emoji to express the confusion and disgust looking at this syntax

@sodiboo right something with a nullable pointer
[l:agez] something(l)
vs something with a non-null pointer
[l:addr | l > null] something(l)

agez being a type alias meaning "address greater or equal to zero", on a non-negative type

@buffet actually you’re right.

while ATS doesn’t look at first glance like what i literally asked for (“Rust but not Rust”), it does seem to have a lot of the properties i care about. i do think you’re right, that ATS is what i wanted to ask for.

i really like its philosophy of needing to prove the correctness of the program. that sounds really useful, actually! i’ve not looked at any substantial code yet as i write this message, thogh, so i don’t know yet if it will feel ergonomic.

an example from one of the first pages of the introduction of an expression which doesn’t evaluate is 1/0. i put this into my editor, and was impressed to see not some complaint about “division by zero”, but instead a much more generalized error about needing to prove the constraint that some expression != 0. that’s really cool! i’ve never seen a language that lets me do this statically (at least, with native performance)

@sodiboo hell yeah
have fun!

@buffet so far ,i’m very intrigued at how many constructs have several different syntax options.

for instance, there are four kinds of comments. two different block comments.

admittedly, this has nothing to do with the type system or semantics. which is why i’m here. so, it’s a boring remark for me to make. still, unusual way to design a programming language.

@sodiboo i also *strongly* recommend
1. ats-acc (https://github.com/sparverius/ats-acc/) for easier to read errors (sadly it hides info you need in some cases)
2. learning what PMVtmpltcstmat means, specifically that peeemveeteeempeeellteeseeessteeemmaytee not defined means you forgot to include the atspre_staload or whatever the file was called, which defined a macro that evaluates to NOTHING, but the compiler emits that :)

@sodiboo also try to guess what it stands for, it's a fun game

@buffet i noticed ats-acc in Nixpkgs but that package was broken(?) so i didn’t think too much of it. but i did try fixing it and indeed ! wow! those errors are much more readable!

here’s my fixed version, for anyone else reading this who happens to run into that same issue:

(pkgs.ats-acc.overrideAttrs (prevAttrs: {
    postPatch = builtins.replaceStrings ["--replace" "-Dm755 acc" ] ["--replace-fail" "-Dm755 acc -t"] prevAttrs.postPatch;
}))

i’d submit a PR to nixpkgs, but, for some reason my local checkout of it seems to be somehow corrupted and i don’t feel like fixing that right now. i should probably be worried about why git fails to fetch nixpkgs. oh well

@buffet i’m reading the docs cover-to-cover and still haven’t gotten into any of the dependent/linear types stuff. that’s some chapters away. but i really like this:

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x1343.html

#define :: list0_cons // writing [::] for list0_cons
#define cons0 list0_cons // writing [cons0] for list0_cons
#define nil0 list0_nil // writing [nil0] for list0_nil

Note that the operator :: is already given the infix status. For instance, the list consisting of the first 5 natural numbers can be constructed as follows:

cons0(0, cons0(1, 2 :: 3 :: 4 :: nil0((*void*))))

this is a very neat way to implement operator overloading? just allow redefining the operator in a scope. like any other name.

in particular, it seems like an “obvious” way to allow a programmer to refine what an operator like + means. in Rust, + on integers is “panic-on-overflow” in debug or wrap in release, and you have various other functions like checked_add, wrapping_add, saturating_add, strict_add to define more precise semantics. and then there’s std::num::Wrapping and std::num::Saturating newtypes that mostly just change which one the + operator refers to. why is that a new type!! it seems to much more elegant to just redefine + in a scope!

Zig has a similar problem to solve. it doesn’t have “operating overloading”, so all operators only work on primitives, and there are several addition operators. +| is saturating, +% is wrapping, and + is just like Rust’s panics-in-debug-but-wraps-on-release. also just like Rust, Zig “kinda sorta” supports changing what + means temporarily. @setRuntimeSafety(false) will (among other things) force + to be wrapping for the duration of that scope. in essence, it redefines + = +% (and some other stuff).
i think it’d be neat to be able to redefine operators within a scope like that in more programming languages. i think it’d also fit in with Zig’s philosophy of “no hidden control flow” because there’s no secret impl operator in a completely different module; it’d be defined right there! in the current scope! and it would make working with non-builtin math types way comfier!

(i’m only comparing this to Zig because i just read their documentation cover to cover, so it’s fresh in my mind to contrast with)

i really like how ATS does operators, at least at a glance.

@buffet i guess i’m mostly thinking out loud to process “what’s the perfect language for me?”. i’m not comparing it to Zig only because i recently familiarized myself with Zig, but because i really like the culture around Zig. its leadership. and a lot of its language details. and i’m used to Rust which also does things right that i really like. and of course, dependent/linear types in ATS sounds awesome.

i’m digesting what i love about each one is all.

@sodiboo i'm not quite sure how "in a scope" that is
but it is very simple and practical :3

@buffet oh of course. i know #define is basically “this name is forever and always”. but like. translating that to something like Zig it would look like const :: = list0_cons, which is scoped.

i realize it isn’t scoped in ATS. or at least, it doesn’t look like it is. but it totally could be with no obvious trouble. it’s a trivial enough change to make that i didn’t even mention it when comparing to “what this would look like in another language”.

@sodiboo mhm! keeps most of the simplicity while only relying on features the language has anyways

haskell also does operators in a fairly similar fashion, where you can just
let (+) = something very cool
in 5 + 3

@sodiboo iirc in haskell an operator is just a function that has a non-alphanumerical name :3

@buffet ya . i was thinking of Haskell too when i saw this.
i guess Haskell does it in a very similar way to ATS? so this isn’t unheard of.

though, as far as i can tell, an operator isn’t a “regular name” in ATS? in Haskell you can curry any operator like (+) 1 2. it’s “just” a function and without arguments, it’s still a valid expression. whereas in ATS there’s the op keyword to do something similar. op+ (1, 2).

so i think this means that a library can’t define operators inherently for a type the same way you could in Haskell. it’s clunkier to “import” an operator overload? which, at the very least in the context of something like Zig, is a desirable trait.

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c1379.html

ooo exceptions are linear. that is something which, feels obvious in hindsight, but not clear at a glance that it “must” be the case. in particular, i’ve seen some literature on linear types and exception handling about bubbling up every linear value in every intermediate scope to the exception handler, and i’ve also considered the idea of forcing a linear declaration to respond to exceptions with some default destructor (like Rust’s Drop, but not allowed to be called on the non-panic codepath). this gives me a third idea of “every linear declaration must handle exceptions, and in many cases it’s okay to wrap the exception in some new linear type containing the inner exception and the resource“. in particular, i’m fantasizing about the idea of taking an entire item out of a linear collection and at an inner scope, handling exceptions by wrapping them with an exception containing this linear item for the purpose of catching it higher up, re-inserting it back into the collection where it was taken out, and then rethrowing the inner exception. but for something like a socket, if communicating over it fails, a more appropriate action upon an exception would be to just close that file descriptor.
this kinda is the thing i’ve read about “force exception handlers to catch every linear value” but like,,, actually practical lol.

and as far as i can tell, what i’ve just described is probably possible in ATS? if that’s the case, then that’s fucking awesome and i’m so excited to get to the chapters where i learn more about doing exactly these kinds of things !!!

@buffet it is somewhat worrying that with every new feature which is introduced, there’s a 50% chance of having the caveat of “actually this is a footgun”

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x1491.html

I consider references a dangerous feature in functional programming

in particular, there have been many allusions to a garbage collector, which is so far required for basically every example i’ve seen, but, allegedly, Linear Types Fix Everything Maybe, and “well-written” ATS programs can be compiled without any garbage collector if they avoid certain language features.

i guess it’s nice that the language is “versatile”? but for my use cases, these are anti-features . and i would prefer to have a simpler language without them.

i will read on, hoping to be freed of worry when i get to the mythical chapters documenting the superpowers of this language .

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x1525.html

As for programming with arrays that carry no size information, it is a topic to be covered after dependent types are introduced.

i feel like i’m being edged.

@buffet

(from same page as parent post)

The functions for converting between the type int and the type size_t are g0int2uint_int_size and g0uint2int_size_int

what the fuck!!!! i get that this is The Hardest Problem in Computer Science and all. but THAT’S THE BEST YOU COULD DO? integer literals don’t even coerce to size_t. i HAVE to spell a size literal as g0int2uint_int_size(4)?? are we fucking for real???

@buffet wait what

in later chapter, they define this:

postfix sz
#define sz(x) i2sz(x)

and now size “””literals””” can be spelled 4sz.

if i2sz is a thing, then what the fuck is a g0int2uint_int_size ??? why do they seem to be interchangeable?

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x1656.html

Handling I/O in ATS properly requires the availability of both dependent types and linear types, which I will cover elsewhere. In this section, I only present a means for allowing the programmer to access certain very basic I/O functionalities.

agaaain,,, i’ m being edgedddd,,,, FILEref isn’t linear !!! i’m not forced to free it !!!

@buffet i’ve finished the first two chapters on functional and practical programming…

and i’m also almost falling asleep !!! it’s taken me so long to get there! i’ve been at this for 8 hours? what the fuck. no wonder i’m tired.

i will take a break. maybe sleep. when i return to this, i will have a great understanding of the fundamentals of ATS and how it relates to C; empowering me to finally start with the goodies on dependent and linear types and theorem proving without feeling lost in the basics of an unfamiliar language.

@sodiboo substituting substitutions 🥴

@sodiboo it is a very unusual language in general^^

a lot of the weirder choices are justifiable by thinking about if hwxi took this from C or ML and specifically when something was mixxed

@buffet @sodiboo there's also F*/Low* (and Idris2, partially Haskell's broken LinearTypes, etc) for linear types and typed memory management
There's stuff based on separation logic if you wanna jump deeper in
One of these days I'll actually learn ATS as well

@tranquillity @sodiboo right i fully forgot about f*/low*
i ran into some issues when i looked into it forever ago, but i should try again!

@buffet @sodiboo the procedure for getting the toolchain working + the documentation are pain concentrate and nonexistent (in this order)

@buffet like a git diff of a patch file.!!

@sodiboo too tired to fully understand, but i think should be possible?
you *can* force something to be handled

@sodiboo yes, lots of edging in general, hwxi's really into that

@sodiboo hahahaha this is actually the function i was looking for when i looked at ats code the other day^^^

@sodiboo https://github.com/githwxi/ATS-Postiats/blob/5e752821de2af56eb1c62399ff7f552ba291ef64/doc/BOOK/INT2PROGINATS/CODE/CHAP_EFFECTFUL/permord.dats#L104

@buffet what the hell !!! who hurt them !!!

@sodiboo hurt people hurt people 😔

@buffet ok time to learn about the interesting/new parts of ATS.

this post serves as a time marker for myself to see how long i’ve been at this. i will now start reading:

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2243.html

@buffet

okay, so earlier when i did 1/0 i found it neat that it threw a generalized constraint error. i then found it very concerning that this function compiled fine:

fun div(x: int, y: int): int = x / y;

(and in fact, it aborts at runtime. doesn’t even throw a well-formed exception or anything. SIGILL)

however, it seems i must opt in to constrant checking by explicitly using dependent types.

they describe an alternative integer type that at first seems to be the same thing:

typedef Int = [a:int] int(a);

but the difference is that this type do not go through unchecked arithmetic

fun div(x: Int, y: Int): Int = x / y;

fails with unresolved constrant y != 0.

neat! excited to see where this goes.

i saw something about balanced b-trees earlier in the book. my vague mental goal now is to define “well-typed” collections of that sort, preventing invalid state (such as unordered keys) with the Type System rather than relying on encapsulation like i’m used to from Every Other Language i’ve used.

@buffet also, unrelated to ATS, but i talked to my friend @nea89 who informed me that apparently Lean is another programming language with similar capabilities. that’s wild !!! i thought Lean was just a proof checker for like, Math Papers. i’ve interacted with it in the form of “The Natural Numbers Game”, but i didn’t realize it was a real language usable for writing practical programs!

next up, i’m probably learning Lean. but for now, i’m definitely gonna commit to ATS for learning this fundamental way of programming.

@sodiboo @buffet @nea89 I wanna watch this live, sodi learns ATS and Lean
Do Agda and Coq too plz
I'd also ask for Idris2 and F* but I already mentioned those before

@tranquillity @buffet @nea89 im liveposting. thats as live as u will get.

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2403.html

i like that the factorial function starts with fun fact ☝. reminds me of fun, safe optimizations

fun
fact{n:nat}

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2428.html

introduction to the String type, which is the dependent version of string

it feels odd that these correctness/“safety” checks are off by default with the primitive types, and that there’s a parallel version of each one holding all the same values. i hope i get introduced to some lint to error out on non-dependent primitives (or something like that), because otherwise i don’t think i can feel comfortable fully trusting myself or the typechecker to guarantee that i’m not doing anything wrong? i should be able to use them when necessary of course, but i “want” that to only be allowed in a limited scope. it feels unsafe {} to me.

@buffet

i’ll be honest most of the string stuff flew over my head. i might need to come back to this. it didn’t feel particularly interesting to me, other than showing some examples of dependently typed C strings, which i guess is the point? but maybe i’m just prejudiced against C strings and that’s why i didn’t care.

In ATS, properly processing C-style strings also makes essential use of linear types, which I will cover in another part of this book

i’m being edgedddd again!!!!!!!

@buffet i am however, thinking about how i’d even represent Rust strings (UTF-8 byte slices). could “safe” indexing of such strings be encoded into this type system? i assume so, but currently i don’t know where i’d even begin with such a thing.

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2475.html

a static integer I (i.e., a static term of the sort int)

this kind of phrasing is reminding me of arithmetic on values encoded as types in Rust and TypeScript, as well as comptime values in Zig (comptime_int in particular). specifically, in the sense that there is a parallel language with very similar types and values, but which has entirely different execution semantics. the “type system” is essentially its own sub-language. (in Zig, they are much closer to being “the same language”, but there are still differences in what types and functions you can use in either context).

@buffet

(from same page)

fun{a:t@ype}
array_make_elt{n:int} (asz: size_t(n), elt: a): arrayref(a, n)

something very interesting i notice here is that size_t takes an n:int, instead of some static n:size_t. so, actually it’s wrong to say that the int in val x: int and [a:int] are the “same type but different”.
they noted that the static term type int is arbitrary precision. and the analyzer reasons about them as such. and it’s neat that size_t takes the same parameter.

forgive the types i invent now to specify bitwidths (i hate C integers), but this means to me that i should be able to prove something like x: u32(n) where n < 256, and then cast it to a u8, with the assurance that there will be no overflow or wrapping or discarded data. it’s a lossless conversion.

it is mildly worrying to me that there is no “overflow error” on e.g. (x: Int, y: Int) => x * y (pseudo-closure-syntax). because like. there should be ? this function is not infallible for all machine-width integers. (unless you define that it wraps twos-complement, but that’s a terrible default interpretation for a target-dependent integer width)

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2550.html

this example of debugging an infinite loop with termination metrics is pretty cool!

By being precise and being able to enforce precision effectively, the programmer will surely notice that his or her need for run-time debugging is diminishing rapidly.

indeed, that does look like it’s true. i might need less runtime debugging in ATS than i would in other languages. and that’s the goal! to catch more stuff at compile time ! that’s what i wanna do !! finally, the stuff i came here for.

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2584.html

here they provide a very long example of list_last, which seemed unnecessarily complex to me. why is the loop explicit here?

i successfully implemented a much simpler version:

fun{a:t@ype}
list_last{n:nat} .<n>.
  (xs: list(a, n)): option(a, n > 0) =
  case+ xs of
  | list_nil () => None()
  | list_cons (x, list_nil()) => Some(x)
  | list_cons (_, xs as list_cons _) => list_last(xs)

this typechecks all the same, and has the same signature.

the only problem i ran into is that | list_cons (_, xs) on the last type does not satisfy the constraint. i have to specify that it’s a list_cons _, even though the compiler can deduce that fact already (because if i remove the line above, the case+ is inexhaustive).

this felt like a bug? an oversight? but in the end, it’s not really too much of an inconvenience. i know that case arm types do not depend on the ones before them. which when put like that, actually sounds like it might be a good thing for readability/maintainability long term in larger codebases.

i really don’t understand why the book implements this function in a much longer way. i guess to reinforce the importance of explicit tail-recursive loops? but my version is also tail-recursive!

@buffet i did have to return to a previous chapter to fresh up on the pattern matching syntax to do this, though. so turns out reading the basics before diving into the deep end was a good idea after all. i’m already finding myself in use of that information, and because i’ve already read it once and indexed it mentally, i can easily find it again!

@buffet oh hey! they address exactly the thing i just talked about just a couple pages later!

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2795.html

this describes exactly the behaviour i observed through experimentation!

@buffet

The use of the symbol =>> (in place of =>) indicates to the typechecker that this clause needs to be typechecked under the sequentiality assumption that the given value matching it does not match the pattern guards associated with any previous clauses.

oh, cool! so my function can be made even shorter by doing this:

fun{a:t@ype}
list_last{n:nat} .<n>.
  (xs: list(a, n)): option(a, n > 0) =
  case+ xs of
  | list_nil () => None()
  | list_cons (x, list_nil()) => Some(x)
  | list_cons (_, xs) =>> list_last(xs)

and indeed that works! honestly, i think it was more readable first way i did it, though. i think i like the default behaviour here, but i’m glad they have the alternative for the more “powerful” behaviour. turns out, this is definitely not an oversight in the compiler implementation as i first thought.

@buffet

oh ! neat! they even explain the rationale

One may be wondering why typechecking clauses is not required to be done sequentially by default. The simple reason is that this requirement, if fully enforced, can have a great negative impact on the efficiency of typechecking. Therefore, it is a reasonable design to provide the programmer with an explict means to occasionally make use of the sequentiality assumption needed for typechecking a particular clause.

yeah that checks out to me. it’s done mainly for compile times. less work by default, because in most cases that work is unnecessary.

i could foresee cases where the DX is better too . defaults are king so it’s nice to see the “stricter” version being the default.

@buffet

i mostly skimmed over the part about RB-trees for now. it is a very intricate example of concept that, i believe, i already understand decently well by this point

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c2867.html

finally ! getting into Theorem Proving!
my prior experience with the Natural Numbers Game in Lean should come in handy here. already, i think those examples of dataprop look vaguely familiar. it has been years since i went through that though, so i’m by no means an expert. but at least, this doesn’t feel like an entirely alien concept to communicate to the computer.

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x2929.html

again, i vaguely recognize the Statements that need to be proven here, and the implementations are intuitive enough to read and write.

because these are “Total Functions” (i.e. non-diverging functions. for any given input they always return some value in a finite amount of time; enforced using termination metrics), i believe that type-checking (which runs in some linear~ish amount of reasonable compile time) suffices to conclude that the statement in the signature is true. dataprop values are not “literally” part of any function that is executed or whose return value is interesting. the value vaguely encodes what axioms are used in the proof maybe? but the fact that it for sure is a value is all we need.

and because this inductive reasoning is only actually verified once per codepath, it’s okay to be wildly abstract and recursive here, because it’s not used at runtime. (nor is the type-checking/verification actually recursive; as long as the “proof codepath” is proven to be finite, verification is only linear~ish)

and this also means to me that, if i can prove certain fundamental properties (“axioms”) about an abstract datatype interface (e.g. “list semantics”), for several given “implementations” (e.g. an array-list/Rust Vec), then i should be able to write generic code that only requires the “list semantics”, but works with linked-cons-lists or dynamic arrays or whatever else i throw at it.

that’s where i THINK this is supposed to inevitably lead. i really hope i get shown examples of things like this. i’m excited to do nontrivial stuff with it.

@buffet
yess

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3264.html

we finally see an implementation that’s generic over a datatype. fast exponentiation that works likewise on scalars or matrices.

i don’t have too much to add here. a lot of these proof chapters have been stuff that i don’t necessarily have much to say about. i’m taking in the information, even if i’m posting slowly.

it’s been very theoretical, and it was previously alluded to that proofs are very useful to reason about actual practical code that works with linear types.

i’m now at this point: https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/p3319.html

based on the headings, i’m guessing “views” are going to be analogous to Rust references, and “viewtypes” are types with particular lifetime-related constraints? maybe? not sure

@buffet

opening paragraph here is badass:

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c3321.html

i’m inferring that there are no constrained “references” per se. it’s raw pointers all the way down. but the type system forces you to provide a proof that any given usage is, in fact, sound. that’s awesome!

having seen the fact that regular functions can return proofs of properties that their return values hold, i assume that “safe” pointer-related functions will have a signature like so:

fun{a:t@ype} read_pointer{p:ptr}(valid: ProofThatPointerIsCurrentlyAlignedAndReadable(Pointer(p)), p: Pointer(p)): a

obviously this is hyper-pseudo-ATS. in particular i know that the proof is supposed to only consist of proofs? perhaps there is still the concept of a “lifetime” to a resource like in Rust? probably this is what views relate to. somehow.

@sodiboo yeah good luck

@buffet

yes, that did seem to be an accurate prediction of what i was going to see in the rest of the page!

something that i probably could’ve intuited is what the common generic element of the proof and the pointer is.

it’s the address!!!! that makes sense!!! and indeed, this “correctly aligned and currently valid” concept i stated, is actually spelled out “there is currently a value of T at this specific address”; and that proof needs to be provided when you read a T from a pointer at the same address.

in particular, i can already see that i should be able to use this exact system to prove something about slices. if i havestart: ptr x, len: size_t y and a proof that [p:addr | x <= p; p < x + y] T @ p, then this is basically equal to a Rust &mut [T] (plus or minus some thread safety semantics perhaps? but if i understand correctly, this proof should be unforgeable if i play my cards right, and if it’s e.g. only acquired through a mutex, the mutex guard is linear, and freeing it requires me to “dissolve” the view proof; then i feel like the usage will be obviously thread safe. so i think actually this is exactly equal to a rust &mut [T] ?)

@sodiboo yup, this is great :3

@buffet i’m very excited to keep reading. finally all this proof stuff is very quickly looking like it’s becoming very applicable to very real practical native programming patterns

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3418.html

hm. this closure representation feels wrong to me.
the function pointer is stored next to the captured environment? in a tuple, both behind the same pointer?
this reads to me that the memory layout must be such that env is stored sizeof(ptr) (e.g. 4) bytes after the function pointer. but env might want a higher alignment than that (e.g. 8). in this case the function pointer must be stored sizeof(ptr) (e.g. 4) bytes before the env. the start of the tuple may therefore be less aligned than the alignment of env. if env is aligned to 8, its lower bits are ?000, and if ptr is aligned to 4, its lower bits are ??00, but because of the layout in the tuple, it must actually have lower bits ?100. the start of the tuple must be aligned with lower bits ?100.

with Rust’s standard Allocator semantics, every allocation can be aligned. but only to powers of 2. that is, you can get an allocation that starts at ????, ???0, ??00, ?000, but the lower bits must all be zero. there is no such thing as an allocation aligned to ?100
therefore, the only way to allocate a cloptr if sizeof(ptr) == 4 and alignof(env) >= 8 is to allocate at least sizeof(env) + alignof(env) (e.g. sizeof(env) + 8) bytes, and waste the first alignof(env) - sizeof(ptr) (e.g. 4) bytes, leaving them unused, then shifting the pointer before using it as cloptr, and remembering to shift it back to the original allocation basis before deallocating.

and this is why the correct representation of a closure is actually {f:addr, e:addr} [env:t@type] ((&env, a) -> b @ f | ptr f, env @ e | ptr e

because then you don’t need to waste space at the beginning of the env allocation, just to put the function pointer inline before the data.

also it saves the function address from needing a double-deref. not sure how much that actually matters.

one downside of this is that a closure is no longer “boxed”. it’s not pointer sized. the correct way to reconcile this is to make a boxed_cloptr(l:addr, a:t@ype, b:t@ype) = [f:addr, e:addr, env:t@ype]((&env, a) -> b @ f | ptr f, env @ e | ptr e) @ l | ptr l (tuple-behind-pointer, but now both fnptr and env are double-refs, instead of env being inine), and use this only when needed in pointer-polymorphic functions.

The very ability to explain within ATS programming features such as closure function is a convincing indication of the expressiveness of the type system of ATS.

indeed!!!! i am actually really happy to see that a closure pointer is “just” a regular type with some linear semantics. i can use a different closure pointer that i think is more correct!! and the language doesn’t mind!!! it’s badass as hell that i can correct the memory layout of something so fundamental as closures in terms of ATS instead of having to abstractly describe what the language does wrong.

ATS closures are just dependently-typed void* user_data which makes them impossible to misuse. that’s fuckin awesome

@sodiboo uh probably best to look at compiler output

i'd assume it just puts everything in a c struct, which means you'd probably end up with padding after the pointer

@buffet no. that’s not possible. that closure code is polymorphic over every type of env. the compiler doesn’t statically know the sizeof(env) in these closures, so can’t assume anything about its alignment and can’t pad it accordingly. and even if there is somehow padding there, that’s just as space-inefficient!

fundamentally, there’s just not really any good reason to keep the function pointer inline with the env. (in the Language I’m Used To, Rust, closures are all unique types that are not interchangeable consisting of just their environment and no function pointer. &dyn Fn() is a reference to that environment, which has “pointer metadata” of the function address (like &[T] points to contiguous memory, but is really like { start: *const T, len: usize }. not { start: *const (usize, T) }.

The Object is the environment. the metadata required to successfully use Said Object is the function address.

thankfully, i don’t have to think about this much further because, again, a closure type isn’t really built into the language? it’s just a Type that you can Express. so i can choose to Express it Differently because i have Opinions. i actually really like that i can do it the way i think is correct.

@sodiboo why would it not be possible? different envs would compile to different structs in C i think

@buffet because it’s not monomorphized. [env:t@ype] is an existential quantifier (not the ATS term for this?) ensuring that certain constraints of the following expression hold for any given type, of any size, env
but to actually use the type containing env, we don’t need to know what env is, its size, or its alignment. we never read any value of env when using the closure.

the whole point of closures is that only the function pointer knows anything about env.

if we knew information about the layout of env, we necessarily know which function that environment is for. because each function requires a unique environment type. therefore, the function pointer is dead code. you can just do a direct call to the actual function that closure environment relates to.

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3475.html

if x is a declared variable of the type T, then a linear proof of the view T?@L, where L is the address of x, must be available when typechecking reaches the end of the scope for x. This requirement ensures that a variable can no longer be accessed after the portion of the stack in which it is allocated is reclaimed as no linear proof of the at-view associated with the variable is ever available from that point on.

yessss!!! this is Literally Generalized Borrow Checking. i now fully agree with your assertion that ATS is what i originally asked for. this singular rule sounds exactly like what Rust lifetimes are supposed to enforce. i asked for Rust-like references and THIS SMELLS VERY MUCH LIKE A BETTER RUST

@sodiboo ah right
hm

@buffet a compiler with such an ABI can generate padding between the first field of env and the function pointer though, if it can require that env itself is ?100-aligned (because then, the first field will be ?000-aligned, and so will the function pointer, and so can the entire allocation be). forcing a type to be ?100-aligned is not allowed under the Rust semantics i’m used to.

i suspect in reality, any code written like that will just misalign the closure environment? to my understanding this is not catastrophic? i think it is the case that “aligned” pointers have performance benefits in hardware, but otherwise exhibit the same semantics as unaligned pointers? but i think my understanding here is probably wrong because i think if it was just slower, languages like Rust and Zig would not be so intent on killing you upon the mere thought of an unaligned read.

(vague grumbling about atomics?)

@sodiboo @buffet some
unaligned accesses may happen to work fine on x86 but this assumption is neither portable nor consistent

@sodiboo @buffet
like the reason why it is not allowed in the rust or zig abstract machine is that misaligned accesses crash the program on some targets and there is no way around that without either requiring all aligned accesses or really slow non-atomic accesses

even on x86 where misaligned access is not just permitted but also not much slower, the compiler might optimize your code to use simd instruction and will use aligned ops that will crash your program

@buffet @sodiboo
this applies mostly to native memory access sizes, but beyond splitting you data <=64 bytes accross multiple cache lines also slower than not doing that

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3475.html

these “flat closure-functions” are not explained in detail. how are they laid out?

from experimentation, they look very close to the garbage-collected -<cloref> things i’ve seen earlier in the book. but they use -<clo> syntax. but even that is not correct. trying to assign a value like so:

val x = 4;
var f: () -<clo> int = lam@ () : int => x;

gives me such an error:

   error: mismatch of static terms (tyleq):
          actual:  () -> (int)  :: [ CLO ]
          needed:  () -> (int)  :: [ CLO ]

i infer that a “flat closure-function” must mean something like Rust’s impl Fn, where the type also encodes which function it is. based on the examples, this seems to be mostly useful as syntax sugar for loops? i don’t think this type is directly usable in a runtime-polymorphic fashion. and it also looks (by the title) like the very next page will show me how to do runtime-polymorphic closures.

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3534.html

val f = lam (x: int): int =<cloptr1> x * len

hm. this is more opaque and magic than i had hoped. there really does seem to be a strong idea here that A Closure Is One Pointer Not Two.
can i not get the env and the fnptr separately? i suppose you wouldn’t want to allow a programmer to move the env, because it might be self-referential (i.e. pinned, see: Rust’s Pin<T>. conveniently moving env is only possible if it impl Unpin)

The support for linear closure-functions in ATS1 is crucial in a setting where higher-order functions are needed but run-time garbage collection (GC) is not allowed or supported. In ATS2, linear closure-functions become much less important as programming with higher-order functions in a setting without GC can be more conveniently achieved through the use of templates

this sounds to me like monomorphized higher-order functions/closures, which i’m excited for.

so far, i’m mildly disappointed to have seen closures introduced as this “DIY” thing, but the actual layout still feels like it’s prescribed by the compiler.
can i not model an idiomatic C interface where a void* user_data is stored in a struct and passed to a function stored next to it, using closures? in Rust, i’d always model that as a trampoline around a &dyn Fn() or something along those lines. but based on the previous page, i had really hoped i could skip the trampoline if i wanted to do the same thing in ATS

@buffet something i also noticed, is that mutable variables are not acceptable closure environment. every closure seems to have “call however many times idc” semantics by default.
I wonder if it’s possible to have a linear environment (and therefore, it’s mutable)?

@sodiboo i'm not sure i've ever used -<clo> tbh

@buffet yes . whatever it is didn’t seem very useful to spell out. but as far as i can tell, it’s almost the inferred type of a stack-allocated lam@()

@sodiboo i mean i assume that it's just gonna have padding to whatever the largest required alignment on on that machine is

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c3811.html

alright. we’re getting somewhere.

i’m disappointed to see that there seems to be an implicit global allocator and deallocation strategy for dataviewtypes? because these are linear and embed dependent constraints/proofs in their types, i would’ve hoped to see a restriction similar to Rust where they must not be self-referential (“infinitely-sized”), and instead have idiomatic use be behind a linear pointer.

though, based on some context clues (and sneak-peeking at actual standard library implementations), i think my interpretation of this page in the book is pessimistic. there does actually seem to be a better concept of custom linear allocation/deallocation?

Note that the tilde symbol (~) in front of the pattern None_vt() indicates that the memory for the node that matches the pattern is freed before the body of the matched clause is evaluated. In this case, no memory is actually freed as None_vt is mapped to the null pointer. I will soon give more detailed explanation about freeing memory allocated for constructors associated with dataviewtypes.

if i understand correctly, this paragraph seems to conflate the idea of “clearing”/“uninitializing” data in memory ( std::ptr::drop_in_place) with actually deallocating the same block of memory. and that’s where my confusion of the implications this has, comes from.

@buffet

The following declaration introduces a linear datatype list_vt, which forms a boxed type (of the sort viewtype) when applied to a type and an integer

argh! it was the bad ending! dataviewtypes have implicit allocation/deallocation semantics. realistically this is fine for most programs (most importantly, it’s deterministic). but ATS said it’s great for kernels! surely i can use linear dataviewtypes with manual allocation/deallocation and handle out-of-memory, right?

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3840.html

i’m once again realizing that i need to take a break again because i’m starting to zone out while reading this. i will go eat and come back to this later. i’ve been at this for 9 hours, hm.

@sodiboo proving something like x < 256 is so simple it's great
you'll love to see that in a later chapter of the book!

@sodiboo when you get an index from some iteration method, that also proves that you *can* access at that point (unsure how this'd look with mutation tbh) which means you can safely access there 👍

@buffet in general, for strings, i’m used to “mutation means allocation”. i find myself much more commonly wanting to parse a string and refer to substrings of it later, than ever do much intricate in-place mutation. if i’m ever creating a dynamic string, it’s almost always concatenatively (append-only), like in the case of string interpolation.

any string mutation apart from append is exceedingly rare in code i find myself writing.

and proving that appending to a UTF-8 string is sound, feels very trivial.

---

the only use case i can even think of where editing a string is particularly useful, is in a text editor. but even then, you’re rarely representing the main buffer as a literal string. usually, you want to use some copy-on-write-ish data structure that maintains an edit history.

@sodiboo @nea89 @tranquillity not live enough! need more updates! straight to my brain!

@sodiboo check out ~ATH its a great language with uhh . lifetimes . yea

@sodiboo @buffet @nea89 yaiii

@sodiboo @buffet @nea89 (as an aside, Lean is not really used often for memory safety models & verifying low level code, is it? I at least haven't seen it done yet I mostly see F* and Coq for this (and ofc Isabelle ig))

@sodiboo @buffet @nea89 F* is used like this for eg. https://github.com/signalapp/SparsePostQuantumRatchet#formal-verification

@buffet i’m considering how I’d model things i’m used to and realizing an issue with ATS’s memory model:

• i didn’t notice any distinction between mutable and immutable views?

to some extent, this can probably be modeled by requiring a proof that a value was unchanged. something like fn dont_change_counter{n:int,l:addr}(counter: int n @ l | ptr l): int n @ l | void. should prove that ! counter keeps its value after calling that function. but there’s no guarantee that it wasn’t changed during that function.

so far i can only prove “i returned the memory to its original value” not “i never mutated it”. that distinction is meaningful in multithreading.

i’m thinking about how to model Rust mutexes and other smart pointers, but it doesn’t seem obviously possible yet.

as far as i can tell, “references” (the & syntax) are syntax sugar for pass-by-value-and-return-them linear proofs that an at-view still holds before and after the function.
but i need a way to prove that it holds for the entire duration of that function.

i hope i will be introduced to an immutable view like this, to which writes are not valid.

or maybe i misunderstood? maybe references are secretly actually just exactly what i just described lol. hm. i should go back and reread that part.

@sodiboo i don't rember fully tbh

@buffet also @nea89 when i gave you the web server response example, you said i actually want a total function, not linear values. and this is true, kind of. but what i actually want is to guarantee that a total function is eventually applied to a value, perhaps multiple values acquired at different times and resolving at different points.

a “total function” in the sense of an ATS proof function is not sufficient. because it forces the return value to occur in the same scope as the input. it requires the caller to be aware of the concurrency model; it requires function coloring.

but a linearly typed API can force applying a total function without prescribing when or how i get there. if a request is consumed only with request.respond(), i can do so in a synchronous function, or i can do it after awaiting arbitrary work (stackless coroutine), or i can suspend execution and resume later (stackful coroutine), or i can thread the request value through callback hell. no matter what my function does, the type system forces me to eventually respond (or maybe leak memory? i could throw it into a reference cycle…).

the only problem with this is that i can’t really imagine a way for enforce termination metrics for such a wildly concurrency-agnostic interface? but guaranteed termination is not as interesting to me as non-panicking. (maybe there is something to be proven about termination of arbitrary concurrency models, though)

so yes, i want almost a total
function, but one that is concurrency-agnostic. something naive like fn(Request) -> Response is not concurrency-agnostic, even if it is total.

i think concurrency-agnostic code is the correct way to write reusable libraries. but a lot of languages don’t lend themselves well to doing so.

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3840.html

xs: &list_vt (a, m) >> list_vt (a, m+n),

hm. given such a signature declaring that it mutates, i think i can be confident that references are not immutable.

i remember now, &T >> U is just syntax sugar for {l:addr} T @ l >> U @ l | ptr l such that i don’t need to explicitly name the address each time.

@sodiboo epic

@buffet

we can largely retain the convenience of pattern matching associated with datatypes while supporting explicit memory management

yes. i can see that. and in fact it looks awesome for like 99% of applications.

but a glaring flaw: dataviewtypes enforce a global default allocator with no failure handling! although memory management is “explicit”, where’s the custom allocation of dataviewtypes!

@buffet i do really like the unfold concept, though, allowing for checked partial initialization of each field. every dataviewtype has a ManuallyDrop typestate sibling generated automatically. that’s awesome.

@buffet

in particular, i’m idly thinking about how i’d do an arena allocation strategy. say i’m doing a compiler and i tokenize a file and every token is kept until that entire file needs to be dropped. pretend it’s not an LSP (no incremental parsing).

i’d want to be able to pass around all the token refs, but then prove that all those views are returned to the allocator, incurring no runtime cost, but guaranteeing that a single total deallocation is absolutely safe. maybe tokens can even point to “sub-tokens” some-how; e.g. a “string token” might have interpolation entities, or a “token tree” with rust lexing semantics. could i say that as long as i have a reference to this one token, the reference to the child token within is definitely valid, but statically consuming all roots into this graph ensures that freeing it as a whole is safe, even if there might be internal references to those objects?

these are the types of things i would love to be able to soundly express.

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x3993.html

The interface for merge-sort is given as follows:

fun{
a:t@ype
} mergeSort{n:nat}
  (xs: list_vt (a, n), cmp: cmp a): list_vt (a, n)

aw man. where’s the constraint in the return type that the list is sorted. boo !!!!

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x4154.html

i don’t think i fully internalized exactly how this implementation works, in particular i’m gonna skip over the last exercise. i might need to return here ish at some point.

turns page

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/c4186.html

i see on the table of contents for this chapter some topics that i’ve been very vocal about wanting to learn more about:

• Memory Allocation and Deallocation
• Locking and Unlocking
• Linear Channels for Asynchronous IPC

finally, concurrency and memory management!

@buffet

https://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/x4302.html

ok so i got carried away and spent 10 hours fighting the proof checker to implement a ring buffer.

given that all my types are very precise and Dependent, i’m fairly certain that it’s correct.

but i cannot for the life of me get it working.

i’m pretty sure the issue has something to do with templates. i don’t know why templates are seemingly breaking everything. but it’s a fucking C source error at the “call out to C as the compiler backend” step.

everything typechecks. my proofs are valid.

but it won’t compile. so i can’t actually test it at runtime

here’s my source code so far.

@buffet also for some reason the compiler insists that any indtegers going through this data structure are linear. i have to “consume” them. because they’re linear. but it’s a goddamn integer. how do i linearly consume an integer. it’s blittable!!!!!

@sodiboo can you send the error?

@buffet yes.

i also have a nix shell. error should be reproducible. nix develop and then acc patscc -D_GNU_SOURCE -DATS_MEMALLOC_LIBC -lc -IATS src -o exe src/*.dats && ./exe. gives me this:

------------------ C COMPILER MESSAGES ------------------

In file included from main_dats.c:15:
main_dats.c: In function ‘mainats_0_void’:
main_dats.c:256:21: error: ‘PMVtmpltcstmat’ undeclared (first use in this function)
  256 | ATSINSmove(tmpref2, PMVtmpltcstmat[0](ringbuf_new<S2EVar(5553)>)(tmp3)) ;
      |                     ^~~~~~~~~~~~~~
/nix/store/zj34hcld6yc0jdzc261agpck73x0hz92-ats2-0.4.2/lib/ats2-postiats-0.4.2/ccomp/runtime/pats_ccomp_instrset.h:276:37: note: in definition of macro ‘ATSINSmove’
  276 | #define ATSINSmove(tmp, val) (tmp = val)
      |                                     ^~~
main_dats.c:256:21: note: each undeclared identifier is reported only once for each function it appears in
  256 | ATSINSmove(tmpref2, PMVtmpltcstmat[0](ringbuf_new<S2EVar(5553)>)(tmp3)) ;
      |                     ^~~~~~~~~~~~~~
/nix/store/zj34hcld6yc0jdzc261agpck73x0hz92-ats2-0.4.2/lib/ats2-postiats-0.4.2/ccomp/runtime/pats_ccomp_instrset.h:276:37: note: in definition of macro ‘ATSINSmove’
  276 | #define ATSINSmove(tmp, val) (tmp = val)
      |                                     ^~~
main_dats.c:256:39: error: ‘ringbuf_new’ undeclared (first use in this function)
  256 | ATSINSmove(tmpref2, PMVtmpltcstmat[0](ringbuf_new<S2EVar(5553)>)(tmp3)) ;
      |                                       ^~~~~~~~~~~
/nix/store/zj34hcld6yc0jdzc261agpck73x0hz92-ats2-0.4.2/lib/ats2-postiats-0.4.2/ccomp/runtime/pats_ccomp_instrset.h:276:37: note: in definition of macro ‘ATSINSmove’
  276 | #define ATSINSmove(tmp, val) (tmp = val)
      |                                     ^~~
main_dats.c:256:51: error: implicit declaration of function ‘S2EVar’ [-Wimplicit-function-declaration]
  256 | ATSINSmove(tmpref2, PMVtmpltcstmat[0](ringbuf_new<S2EVar(5553)>)(tmp3)) ;
      |                                                   ^~~~~~
/nix/store/zj34hcld6yc0jdzc261agpck73x0hz92-ats2-0.4.2/lib/ats2-postiats-0.4.2/ccomp/runtime/pats_ccomp_instrset.h:276:37: note: in definition of macro ‘ATSINSmove’
  276 | #define ATSINSmove(tmp, val) (tmp = val)
      |                                     ^~~
main_dats.c:256:64: error: expected expression before ‘)’ token
  256 | ATSINSmove(tmpref2, PMVtmpltcstmat[0](ringbuf_new<S2EVar(5553)>)(tmp3)) ;
      |                                                                ^
/nix/store/zj34hcld6yc0jdzc261agpck73x0hz92-ats2-0.4.2/lib/ats2-postiats-0.4.2/ccomp/runtime/pats_ccomp_instrset.h:276:37: note: in definition of macro ‘ATSINSmove’
  276 | #define ATSINSmove(tmp, val) (tmp = val)
      |                                     ^~~
main_dats.c:266:41: error: ‘ringbuf_insert’ undeclared (first use in this function)
  266 | ATSINSmove_void(tmp4, PMVtmpltcstmat[0](ringbuf_insert<S2EVar(5556)>)(ATSPMVrefarg0(tmpref2), tmp5)) ;
      |                                         ^~~~~~~~~~~~~~
/nix/store/zj34hcld6yc0jdzc261agpck73x0hz92-ats2-0.4.2/lib/ats2-postiats-0.4.2/ccomp/runtime/pats_ccomp_instrset.h:284:39: note: in definition of macro ‘ATSINSmove_void’
  284 | #define ATSINSmove_void(tmp, command) command
      |                                       ^~~~~~~
main_dats.c:266:69: error: expected expression before ‘)’ token
  266 | ATSINSmove_void(tmp4, PMVtmpltcstmat[0](ringbuf_insert<S2EVar(5556)>)(ATSPMVrefarg0(tmpref2), tmp5)) ;
      |                                                                     ^
/nix/store/zj34hcld6yc0jdzc261agpck73x0hz92-ats2-0.4.2/lib/ats2-postiats-0.4.2/ccomp/runtime/pats_ccomp_instrset.h:284:39: note: in definition of macro ‘ATSINSmove_void’
  284 | #define ATSINSmove_void(tmp, command) command
      |                                       ^~~~~~~
main_dats.c:271:36: error: ‘ringbuf_remove’ undeclared (first use in this function)
  271 | ATSINSmove(tmp6, PMVtmpltcstmat[0](ringbuf_remove<S2EVar(5560)>)(ATSPMVrefarg0(tmpref2))) ;
      |                                    ^~~~~~~~~~~~~~
/nix/store/zj34hcld6yc0jdzc261agpck73x0hz92-ats2-0.4.2/lib/ats2-postiats-0.4.2/ccomp/runtime/pats_ccomp_instrset.h:276:37: note: in definition of macro ‘ATSINSmove’
  276 | #define ATSINSmove(tmp, val) (tmp = val)
      |                                     ^~~
main_dats.c:271:64: error: expected expression before ‘)’ token
  271 | ATSINSmove(tmp6, PMVtmpltcstmat[0](ringbuf_remove<S2EVar(5560)>)(ATSPMVrefarg0(tmpref2))) ;
      |                                                                ^
/nix/store/zj34hcld6yc0jdzc261agpck73x0hz92-ats2-0.4.2/lib/ats2-postiats-0.4.2/ccomp/runtime/pats_ccomp_instrset.h:276:37: note: in definition of macro ‘ATSINSmove’
  276 | #define ATSINSmove(tmp, val) (tmp = val)
      |                                     ^~~

-------------- END C COMPILER MESSAGES ------------------

i find this StackOverflow question about the same symbol. solution is “don’t define calloc wrong”. but i’m not binding to something that already exists. this error is in code that i’m defining. so “don’t ever use templates” isn’t very applicable advice i reckon

@sodiboo write a function that just eats it

@sodiboo like obviously don't, but

@buffet ?that’s what i did lol

@sodiboo you fool! what i did i tell you about PMVtmpltcstmat when i introduced atc-acc?

internal compiler macro used to add template expansions or something that expands to nothing

you forgot some prelude header

@buffet which one, though! the point of a prelude is that it’s supposed to be implicit!!???

@buffet you did indeed mention that macro

@buffet and I’ll have you know. i am literally importing atspre_staload!!!!

see literal fucking line one:

https://turning.computers.gay/sodiboo/playing-with-dependent-types/src/commit/458c686293353c5c6d5db9b64f24bf4ace47f871/src/main.dats#L1

@sodiboo yeah idk i never got this part of ats
in my mind this is in "this must never happen" territory along at least 3 axes

@sodiboo there's a reason i have PMVtmpltcstmat memorized all these years later

@sodiboo yeah it's defined somewhere, just get that 👍👍

@buffet what? i’m importing it and it’s still not defined though!! i grepped for PMVtmpltcstmat in the distribution of ATS and didn’t find anything useful

can you like, be more specific about this? ideally, can you provide a diff such that my code builds fine?

@sodiboo uh i cannot, i forgor
i'll try to get it to compile when i'm on computer

@sodiboo i forgor

@sodiboo wait i'm confused, i remember this being a macro that takes a type and a value and returns the value or similar, but that wouldn't even work syntactically with the array index, would it?

@buffet no i don’t think it would

@sodiboo uh so maybe this is the result of type params not being applied or resolved correctly, also the reason you get back a linear size_t is probably because {a:vt@ype}

@buffet but size_t is not linear!!!

yes, the collection is genetic over viewtypes. generic a is linear. but specific a shouldn’t have to be linear!!!

@sodiboo i've no idea