attached type parameters

[aep]

generic containers work, but i still hate them somehow. i thought not knowing the interior type is fine because thats what golang does too, but then golang has reflection so you can get the interior at runtime.

this is unfixably unsafe

new+10  v = map::make();

u8 val =12;
v.insert("hello", &val);

u64 * bad = v.get("hello"); 

well , not unfixable, vec could just store the typeid, but then it's checked at runtime, which is terrible.

new+10  v = map::make();

u8 val =12;
v.insert("hello", &val);

u64 meh;
v.get("hello", &meh);

typestate would help

struct Vec+t {   
}

theory item (Vec self) typeid;

pub fn get(Vec+t mut * self)  void  *
  model  typeid(return) == item(self)
{
}

pub fn main() {

  new+10  v = vec::make();
   static_attest(val::item(&v) ==  typeid(u8));

   u8 val =12;
   v.push(&val);

   u64 * bad = v.get("hello"); // error: implicit cast of  void pointer to different type 
}

this elegantly fits into the powerful smt theories, but it doesn't answer the question of how to decode a struct from json

struct Foo {   
  Vec::vec+100 something;  // dunno which type is in this
}

Other languages do "templates" so they just create a new type for each possible parameter. That's horribly inefficient, as each instance also has to have all of its functions duplicated. It also doesnt map to C.

Instead i'm proposing to just attach the interiour typestate to the external typestate permanently somehow, creating a new virtual type. That's essentially just what tail already is, a permanent type state.

One possible syntax is just reusing the familiar template angled brackets. however, the tail marker has to go somewhere

struct Vec<typeid Item>
struct Vec+t<typeid Item>
struct Vec<typeid Item>+t
struct Vec<typeid Item, +t>


pub fn get (Vec<Item, +t> mut * self)  void<Item> *
{
}

pub fn main() {
    new<u8,+10>  v = vec::make();

    u8 val =12;
    v.push(&val);

    u64 * bad = v.get("hello");  // error: implicit cast of  void<u8> pointer to wrong type 
}

benefit is, it looks immediately familiar. disadvantage is that the familiarity is a trap. This is not a template, and you cannot actually use it in place of a typename.

struct VecWrapper<typeid Item> {
    Vec<Item> inner; // ok
    Item example;      // nope, Item is a typeid, not a type
}

i personally also think angled brackets are a terrible syntactical choice because they're also math operators, but that's what the world agreed on, so be it. We could of course use square brackets or whatever.

struct Vec[typeid Item, +t]

another way to deal with this is creating a way to make integrity theories permanent somehow.

  struct Vec+t {}

  theory item (Vec self) typeid;

  type ByteVec = Vec+t
     where item(self) = typeid(u8)
  ;


  struct A+
  {
    ByteVec+ buffer;
  }

it's difficult to decide between these two options. Allowing a type alias that includes a permanent smt theory is very powerful, but also difficult to understand. The type "templates" are immediately obvious.

[aep]

@wrl

[jwerle]

Knowing the interior type for things like Vec is definitely important. Is typeid in theory syntax supported at the moment?

I like the usage of '[]' instead of '<>' because of the template syntax trap you mentioned. Readers, new comers, and possible new contributors will need this called out.

Permanent theories look interesting, but hard to follow based on the syntax in the example above.

[aep]

TLDR

this is how it'll hopefully look like

struct A+ {
   Vec<item = int, + > v;
}

---

i'm stuck figuring out how attached parameters and smt expressions mix, so here's a longer braindump

this is fine

export fn push(Vec<A> *self)
   where A !=  typeof(int)

but you cannot deconstruct a nested type

export fn push(Vec<Map<String, A>> *self)
   where A != typeof(int)

because

1. A is ambiguously either a type or a bind
2. there's no way to specify another push(Vec). you can only have one function with that name

so the only sure way is interior type access in smt expressions

export fn push(Vec *self)
   where map::value(vec::item(self)) !=  typeof(int)

that solves 1, but it does not solve 2
and maybe you actually wanted to use the type at runtime for something

export fn push(Vec<Map<String, A>> *self)
{
    let more_mem = sizeof(A);
}

so the best way i can come up with right now is make callsite generated arguments explicitly available to user code (the'res currently only the builtin callsite

export fn push(Vec *self, typeid X)
   where X = map::value(vec::item(self))
{
    let more_mem = sizeof(A);
}

note the assign = instead of compare == indicating this is assigned from evaluation in the callsite

callsite generation is something you normally never use, so its ok to require some more advanced understanding of the smt call order. For daily usage, we can shortcut the permanent typestate expression

struct Vec {
}
theory item(Vec self) typeid;


pub fn main() {

   vec::Vec<vec::item = int, +100> v;

   new <vec::item = int,+100> v = vec::make()
   
   static_asset(vec::item(v) == int);
}

at least i hope i can make this work. it requires being able to skip typeof().
the expanded expression looks like this:

   Vec<vec::item(self) == typeof(int), tail(self) == 100> v;

this is a full smt expression, so we basically have touring complete types. It's mind bending actually.

it might be possible to reduce the shortcut further by assuming unqualified names inside an angled bracket refer to the same module as the exteriour.

struct A {
   Vec<item = int, +100> v;
}

[jwerle]

Wow! The power behind this would be powerful, if possible. I like the syntax

…

On Fri, Sep 11, 2020, 12:24 Arvid E. Picciani ***@***.***> wrote: i'm stuck figuring out how attached parameters and smt expressions mix. this is fine export fn push(Vec<A> *self) where A != typeof(int) but you cannot deconstruct a nested type export fn push(Vec<Map<String, A>> *self) where A != typeof(int) because 1. A is ambiguously either a type or a bind 2. there's no way to specify another push(Vec). you can only have one function with that name so the only sure way is interior type access in smt expressions export fn push(Vec *self) where map::value(vec::item(self)) != typeof(int) that solves 1, but it does not solve 2 and maybe you actually wanted to use the type at runtime for something export fn push(Vec<Map<String, A>> *self) { let more_mem = sizeof(A); } so the best way i can come up with right now is make callsite generated arguments explicitly available to user code (the'res currently only the builtin callsite export fn push(Vec *self, typeid X) where X = map::value(vec::item(self)) { let more_mem = sizeof(A); } note the assign = instead of compare == indicating this is assigned from evaluation in the callsite callsite generation is something you normally never use, so its ok to require some more advanced understanding of the smt call order. For daily usage, we can shortcut the permanent typestate expression struct Vec { } theory item(Vec self) typeid; pub fn main() { vec::Vec<vec::item = int, +100> v; new <vec::item = int,+100> v = vec::make() static_asset(vec::item(v) == int); } at least i hope i can make this work. it requires being able to skip typeof(). the expanded expression looks like this: Vec<vec::item(self) == typeof(int), tail(self) == 100> v; this is a full smt expression, so we basically have touring complete types. It's mind bending actually. it *might* be possible to reduce the shortcut further by assuming unqualified names inside an angled bracket refer to the same module as the exteriour. struct A { Vec<item = int, +100> v; } — You are receiving this because you were assigned. Reply to this email directly, view it on GitHub <#121 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AALFFPPAHDGXWY355JZ4KBLSFJFLDANCNFSM4RE5TOBQ> .