Alice ✨

it goes well with the spaghetti

that's out of date actually! it used to do that but these days ImpredicativeTypes exists and ($) is representation polymorphic so it doesn't need to

btw, did I mention that because vega doesn't have references, fields don't have to be contiguous? I.e. the compiler could totally represent ((a,b), c) like (a, c, b)
(although it doesn't do anything like that yet because non-contiguous fields kind of complicate the compiler ^^)

i'm pretty sure ghc can even optimize one into the other because they *are* semantically equivalent! (but don't quote me on that)

well, `f x = if blah x then g else h` isn't (in a pure, lazy/total setting) any different than `f x y = if blah x then g y else h y` though. you know just as much about what's being executed.

okay great! that's what i'm doing in vega and i got worried for a second that i'd have to rewrite the layout generation code again ^^

However, their endgame isn't to eliminate human labor (I doubt they would for software engineering). The final outcome of this general trend is them inserting themselves as a gratuitous extra step in the process where people babysit agents and pretend the agents did all the work

hmm interesting! does it make sense to have a separate stride value though? like, are there cases where stride isn't just size rounded up to the next multiple of alignment?

(so: i guess "feature" although i think currying is kind of silly in general)

in a pure setting there is (almost) no meaningful difference between those! (that's kind of the idea behind currying ^^)
in an impure setting it could be bad because the function could do something before returning the function for the next argument but in practice noone does that

well that doesn't apply in rust though because in rust `Puppy` will have size 16, not 9 *because* of alignment. it only has size 9 if you give it `repr(packed)` but in that case you would probably also want it to be stored unaligned (but packed more tightly) in an array wouldn't you?

what is the reason to want a different stride?

like, you know that thing about how rust iterator loops are faster than for loops because they skip the bounds check? in vega, the for loop can skip the bounds check as well! (as long as you iterate over the indices as `Index(n)`s)

in particular, what's really cool about this is that this is safer, often more convenient *and* more efficient than regular bounds checked arrays!

maybe enforcing a `!` on aliases helps with that, maybe not. but i'm really happy with this API either way

it will probably be less noisy than having the full existential, but my concern is that the difference between `Array` and `AnyArray` might be a bit confusing if you don't know how it works. especially since `AnyArray!(Int)` will still show up as `Array(n, Int)` in error messages.

the only thing i'm still not 100% sure of is if i want an alias `type AnyArray!(a) = exists (n : Nat). Array(n, a)`. (possibly with a different name...)

this literally has exactly the same representation as a concrete `Array(..., a)` and because vega supports full implicit existentials, you can just use the regular array functions (and in particular `checkBounds`) on existentials over arrays!
(this is like 90% of why i wanted existentials in vega)

if you don't statically know the length (like in most cases really), you can just use an existential, as in

filter : forall (n : Nat) a. (Array(n, a), a -> Bool) -> exists (m : Nat). Array(m, a)

but if you statically know that your indices are in bounds, you don't need a bounds check! (for example with `mapWithIndex : forall (n : Nat) a b. (Array(n,a), (Index n, a) -> b) -> Array(n, b)`

and where you can index it with a *total* function `index : forall (n : Nat) a. (Array(n, a), Index(n)) -> a`. (with Index(n) as [0,n) )
In the most general case, this moves the bounds check from the array to the index (with `checkBounds : forall (n : Nat). Int -> Array(n, a) -> Maybe (Index n)`).

i mostly thought of this in the context of vega's array API (that isn't implemented yet).
what's pretty unique about vega is that the default array is going to be a size indexed array where `[1,2,3]` has type `Array(3, Int)`...

and if something is *not* visibly a type alias, you can assume that it's generative! (as long as it's not a type family or similar i guess but you'd probably want the same syntax for those anyway)

if you see `sum : IntArray -> Int`, that doesn't tell you anything about what exactly you can pass in (e.g. an `Array(Int)`) or not, but if you see `sum : IntArray! -> Int` you at least know that you need to look up the definition of `IntArray` to find out!

the main problem with type aliases is that in order to understand code that uses them, you need to know what they're defined as.
but usually you don't even know that that's something you need to know because you don't know that your type is an alias.

weird PL syntax idea: maybe type aliases should have some special syntax to distinguish them from regular types? (something like `sum : IntArray! -> Int` with `type IntArray! = Array(Int)`)

oh that's a good point! java people sometimes spell out the type though (like `List#addAll(Collection)` vs `List#addAll(int, Collection)`)

it's so wild how i got into elm just after 0.19 released when everyone was still worried about the language changing too much too quickly and yet it's still in exactly the same state today

with text/bytesting the real issue (imo) is that Lazy{Text,ByteString} are just incorrectly named.
they're not just lazy versions of the regular types (whatever that even means), they're specifically pure Text/Byte *streams*.
like, they have wildly different complexities than the strict versions!

that's arguably HLS's (and Haddock's) fault though because ghc will always disambiguate them in error messages

idk I don't really mind it with vector (where I always use it as `Unboxed.Vector` or `Storable.Vector` anyway) but it's annoying with other libraries