thorin2

thorin2 copied to clipboard

Plz first give #273 your blessing.

• removes block expressions: { d* e }. simply use d* e instead and if you really want to use delimiters use a tuple: (d* e)
• abc::(a: A, b: B, c: C) -> (a: A, b: B, c: C)::abc. This is simpler to parse and makes more sense as the identifier abc is only available after having processed the whole tuple pattern.

abc::(a: A, b: B, c: C) -> (a: A, b: B, c: C)::abc.

I think this syntax is confusing. : is used as type annotation. Hence, we used :: as name :: destructor pattern. Which was okay as it conceptually was somewhat similar to the type pattern. However, with both swapped, it becomes even less clear. Furthermore, :: is commonly used for lists or type hints in Haskell.

I think a syntax like as would be clearer. (a: A, b: B, c: C) as abc means we have the destructured tuple (a,b,c) but also identify the whole expression as abc.

abc::(a: A, b: B, c: C) -> (a: A, b: B, c: C)::abc.

I think this syntax is confusing. : is used as type annotation. Hence, we used :: as name :: destructor pattern. Which was okay as it conceptually was somewhat similar to the type pattern. However, with both swapped, it becomes even less clear. Furthermore, :: is commonly used for lists or type hints in Haskell.

I think a syntax like as would be clearer. (a: A, b: B, c: C) as abc means we have the destructured tuple (a,b,c) but also identify the whole expression as abc.

I tried as but I think it feels quite clumsy - especially when destructing arguments of a curried function:

.ax %mem.load:  Π .[T: *, .Nat] .as Tas [%mem.M, %mem.Ptr Tas] -> [%mem.M, T], normalize_load;

Any other ideas?