3 ms·

I'm working on one [1] and doing the inference now, which is kicking my ass TBH, so some thoughts: > 1) Full type inference. Really, while writing and hacking

by ben509 7y ago

I'm working on one [1] and doing the inference now, which is kicking my ass TBH, so some thoughts: > 1) Full type inference. Really, while writing and hacking, you want it, but ideally the system should be able to fill in your types for you. Note, though, that there's a tradeoff: the more overloading and other conveniences, the less complete the inference can be. In the system I'm working on, it's intended to deploy a library + documentation, so all types would be annotated in the artifact generated regardless of whether they are in the source. > 2). Value types in structures would need to be nominal, not structural. My answer to this is we want cheap sum types. In Tenet, a sum type can be constructed without any declaration by writing tag~expr. This implicitly defines Union[tag~WhateverExprTypeIs]. Since unions implicitly combine, if I have one branch return meters~55 another can return error~"something broke" and the return type overall is implicitly Union[meters~Integer, error~String]. The idea of declaring that, e.g. meters~X and centimeters~Y are interchangeable representations of the same value is something I'm thinking about; it's getting at a facility for encapsulation. > 3) Collections of [product types] would need to be inclusively typed, not exclusive. So, if we have syntax for retrieving an attribute `x.a + x.b` and we know + takes integers, we can deduce an assertion that x is some product type with two integer attributes a and b. I call that an open tuple, as opposed to a closed tuple. But all product types must be closed (exclusive) in order to construct them, obviously, and for non-dynamic languages, it seems like you're liable to have code size explosion (multiple copies of functions to support each type used) if you allow polymorphism this way. > 4) ... it would be important to have all these structural members be namespaced as well. I'm curious what people think the best namespace schemes are, because most of them seem like a lot of complexity for what they do. But... > 5) Now I would still need basic set logic for these types It won't make the first cut, but the basic operations would be sum and diff (for sum types), times and project (for product types) and a renaming facility with globbing seems like it might answer #4 just fine. [1]: https://tenet-lang.org/types.html#tenets-approach https://tenet-lang.org/types.html#tenets-approach

CuriousSkeptic 7y ago
I found it interesting that you tag the types like that. I’m working on a small language idea right now where I wanted to treat bindings as first class, and having them combine with row polymorphism into a construct subsuming tuples, argument lists, and environments into a kind of unified thing, with a similar result in mind. Even to the point of perhaps demoting scalars from first class status actually, point being that where there is a value there should be a name (borrowing the rdf model here) So (n1: v1) might be a value v1 bound to n1. And (n2: v2) another. (n1: v1)(n2: v2) = (n1: v1, n2: v2), and one could even imagine (n1: v1, n2: v2)(n3: n1+n2) as a valid expression. Which of course is equivalent to ( n1: v1, n2: v2, n3: n1+n2, ) not entirely unlike a let-expression (I’m thinking of unifying terms and types so a lambda would simply be such an expression where v1 and v2 are types) Oh well just a toy in my head at the moment. Just found it interesting to see similar tag combining semantics. (As for namespace I was thinking to borrow the plan9 approach of binding things dynamically, using something like Scalas implicits, for evaluation to do a kind of dependency injection thing, but a global lexically scoped tree for typing it)
- ben509 7y ago
  My motivation was to try to accommodate the way I've seen people think and work. So the type system lets you describe anything using literal expressions, and if you match everything up, it should Just Work, or at least have intelligent complaints. (I hope.) So a discriminated union is just a tag stuck in front of something else. > Even to the point of perhaps demoting scalars from first class status actually, point being that where there is a value there should be a name In theory, an integer is just an uncountable enumerated type. I haven't done that to treat it as opaque / atomic, but you could imagine it essentially being 1~~, 2~~, 3~~, etc. But that might come back if I want to have sane semantics of floats, as in not treating NaN as a magic value that doesn't equal itself. > I wanted to treat bindings as first class, and having them combine with row polymorphism into a construct subsuming tuples, argument lists, and environments into a kind of unified thing, with a similar result in mind. This might be helpful just as something to think about, but there is already an example of One Structure to Rule Them All: relations from the relational algebra. (You want to consider the mathematical definition; SQL tables break stuff because of legacy.) A relation can naturally represent any container, but also any function if you allow them to be infinite. So if you have a relation that states all values of y = cos(x), you can join it with an existing expression to apply the `cos` function. (Or `acos` if the system is clever enough.) And that, obviously would get translated into actual function calls. > So (n1: v1) might be a value v1 bound to n1. ... I had to read that a couple of times, but I think I get it. I think being able to combine structures makes a lot of sense, and it's one of those ideas that's not implemented in most languages (as the OP mentions) so we people tend to engineer around the lack of it, so it'd be interesting what idioms develop with it. > As for namespace I was thinking to borrow the plan9 approach Thanks, I'll have to look into that!
  - CuriousSkeptic 7y ago
    Yeah, must confess to being inspired by the relational model. Re: plan9, this is in the context of language I imagine as a kind of interactive environment (think small talk) and where partial evaluation would be the means to construct deployable artifacts. In this environment i expect to support metaprogramming and reflection, typing and unit-tests as something very dynamic and integrated, but purely design time thing. Again, not entierly unlike how you work with a relational dbms system and its schema.

by ben509 7y ago

CuriousSkeptic 7y ago

I found it interesting that you tag the types like that. I’m working on a small language idea right now where I wanted to treat bindings as first class, and having them combine with row polymorphism into a construct subsuming tuples, argument lists, and environments into a kind of unified thing, with a similar result in mind. Even to the point of perhaps demoting scalars from first class status actually, point being that where there is a value there should be a name (borrowing the rdf model here) So (n1: v1) might be a value v1 bound to n1. And (n2: v2) another. (n1: v1)(n2: v2) = (n1: v1, n2: v2), and one could even imagine (n1: v1, n2: v2)(n3: n1+n2) as a valid expression. Which of course is equivalent to ( n1: v1, n2: v2, n3: n1+n2, ) not entirely unlike a let-expression (I’m thinking of unifying terms and types so a lambda would simply be such an expression where v1 and v2 are types) Oh well just a toy in my head at the moment. Just found it interesting to see similar tag combining semantics. (As for namespace I was thinking to borrow the plan9 approach of binding things dynamically, using something like Scalas implicits, for evaluation to do a kind of dependency injection thing, but a global lexically scoped tree for typing it)

ben509 7y ago
My motivation was to try to accommodate the way I've seen people think and work. So the type system lets you describe anything using literal expressions, and if you match everything up, it should Just Work, or at least have intelligent complaints. (I hope.) So a discriminated union is just a tag stuck in front of something else. > Even to the point of perhaps demoting scalars from first class status actually, point being that where there is a value there should be a name In theory, an integer is just an uncountable enumerated type. I haven't done that to treat it as opaque / atomic, but you could imagine it essentially being 1~~, 2~~, 3~~, etc. But that might come back if I want to have sane semantics of floats, as in not treating NaN as a magic value that doesn't equal itself. > I wanted to treat bindings as first class, and having them combine with row polymorphism into a construct subsuming tuples, argument lists, and environments into a kind of unified thing, with a similar result in mind. This might be helpful just as something to think about, but there is already an example of One Structure to Rule Them All: relations from the relational algebra. (You want to consider the mathematical definition; SQL tables break stuff because of legacy.) A relation can naturally represent any container, but also any function if you allow them to be infinite. So if you have a relation that states all values of y = cos(x), you can join it with an existing expression to apply the `cos` function. (Or `acos` if the system is clever enough.) And that, obviously would get translated into actual function calls. > So (n1: v1) might be a value v1 bound to n1. ... I had to read that a couple of times, but I think I get it. I think being able to combine structures makes a lot of sense, and it's one of those ideas that's not implemented in most languages (as the OP mentions) so we people tend to engineer around the lack of it, so it'd be interesting what idioms develop with it. > As for namespace I was thinking to borrow the plan9 approach Thanks, I'll have to look into that!
- CuriousSkeptic 7y ago
  Yeah, must confess to being inspired by the relational model. Re: plan9, this is in the context of language I imagine as a kind of interactive environment (think small talk) and where partial evaluation would be the means to construct deployable artifacts. In this environment i expect to support metaprogramming and reflection, typing and unit-tests as something very dynamic and integrated, but purely design time thing. Again, not entierly unlike how you work with a relational dbms system and its schema.