why are curly and square brackets not the same behavior?

[nilehmann]

@Samir-Rashid asked over Slack

why are curly and square brackets not the same behavior? I thought [ ] desugars to the latter #[flux::field(bool[configured_1])] // syntax same meaning as {v: v == configured_1}

Dumping my response here for future reference

--

An indexed type ([]) is a more fundamental notion, so in fact, the opposite is true, {} desugars to [] (plus an existential type)

We don't have program values in the logic because they are complex and not automatable (they have a memory layout, carry ownership of memory, ...). Instead, we only have pure values (supported by z3) that model an underlying program value. An indexed type T[v] refers to a (program) value of type T modeled by the (logical) value v. Every type T has a corresponding sort in the logic and must be modeled/indexed by values of that sort. For example, if we index/model vectors by their length, the type Vec<i32>[n] refers to vectors whose length is n.

Once you have program values separated from their logical indices you can parameterize over the indices. For instance, consider the following signature

fn is_pos(n: i32) -> bool[n > 0] 

This desugars to the function type for<n: int> fn(i32[n]) -> bool[n > 0]. In words, for every (logical) integer n, if you give me an i32 equal to (modeled by) n, I'll give you back a bool equal to n > 0. The @ syntax also desugars to these universally quantified indices.

The curly brace syntax desugars to existentially quantified indices. More precisely, i32{v: p(v)} desugars to {v:int. i32[v] | p(v)} . The syntax {v:σ. T | p} is a more general syntax for existential where σ is a sort, T is any type that mentions v, and p is a predicate over v. With this more general syntax, you can express stuff like vectors of length n where all elements are less than the length: {n:int. Vec<{v:int. i32[v] | v < n}>[n] | true }

Now, by the way quantifier works there are many types that are syntactically different but semantically equal. For example, and existentially quantified index in input position can always be made into a universally quantified index. For instance, consider the two following signatures

fn take_pos1(x: {i32[@v] | v > 0})
fn take_pos2(x: i32{v: v > 0})

They desugar respectively to

for<v:int> fn({i32[v] | v > 0}) -> ()
fn({v:int. i32[v] | v > 0}) -> ()

i.e., in the first one v is universally quantified for the entire scope of the function while in the second v is only (existentially) quantified in the input. The two signatures are equivalent though, which makes sense if you read it logically because ∀x. p => q is equivalent to (∃x. p) => q (if q doesn't mention x)

Similarly, the type T[e] is semantically equal to T{v: v == e}. So for most the most part, they will behave the same, but for technical reasons related to the way we instantiate quantifiers we put some syntactic restrictions that would require you to write T[e] instead of T{v: v == e} in some cases (in T[e] , the expression e is what we call a value-dependent position)