4 ms·

> Stamps are a kind of micro-types that exist just within the compiler. Like all types they represent information about values, but unlike types you’ve usually

by jhgb 5y ago

> Stamps are a kind of micro-types that exist just within the compiler. Like all types they represent information about values, but unlike types you’ve usually worked with, stamps can give us a variety of properties, such as whether an object can be null or not, or whether a value is positive or negative, or even which individual bits are set in an integer. ...so, they're just types - they define sets of values. Not quite sure why one would have to call it "a kind of micro-types". Especially when it's not even clear what a "micro-type" should be.

dmurray 5y ago
Well, at the very least, Ruby already has a type system so it's convenient to call these something different. And while you're correct that the stamps appear to be an alternative type system, for most people these types will be "unlike types you’ve usually worked with", because most people aren't heavily into Haskell or ML or other languages where it's natural to construct complex type systems like this.
- lmm 5y ago
  > And while you're correct that the stamps appear to be an alternative type system, for most people these types will be "unlike types you’ve usually worked with", because most people aren't heavily into Haskell or ML or other languages where it's natural to construct complex type systems like this. That ultimately causes more confusion though. These really are nothing more or less than types and you can do this kind of thing in a plain old type system and it's actually a lot easier and more effective. Maybe if enough people hear about types we can eventually drag programming culture kicking and screaming into the 1980s.
pugio 5y ago
Coming from traditional statically typed languages (Java, C++, Typescript, even Python or Ruby...), you might think of a type like "int" or "Float". He's calling stamps "micro-types" because they're more fine-grained than that. A stamp might tag a value as being between 0 and 255, for example, which is much more specific than "int". It would be really cool to work with a language that allows the user such fine-grained types, which is one reason I keep eyeing Idris.
- jhgb 5y ago
  > A stamp might tag a value as being between 0 and 255, for example, which is much more specific than "int". Yeah, that's a normal type. For example in Common Lisp, it's the type defined by the type specifier (INTEGER 0 255).
  - chrisseaton 5y ago
    A simple range is one application you could use stamps for, but they can also represent that individual bits may or may not be set, or could even represent that individual bits are set with a given probability, which could inform scheduling decisions.
    - jhgb 5y ago
      Those things can in principle be expressed with a predicate using the SATISFIES type specifier, but the problem with that is that you currently can't pick such types apart for optimization purposes in any existing implementation, only test membership for values. Presumably that's one of the reasons why Qi/Shen was created.
- brundolf 5y ago
  TypeScript can... sort of do that. They could definitely take it further if they wanted to For example a type could be `0 | 1 | 2 | 3 | 4 | 5`, though there's no way right now to specify that as `0..5`
- CorrectHorseBat 5y ago
  Ada can do that
chrisseaton 5y ago
They’re non-nominal - you can’t name them in the language being compiled. They work at a finer level than the nominal system the programmer has access to. (I’m not a type theorist though.)
- jhgb 5y ago
  Hmm. I usually see "nominal" in this context as "matched on basis on type name", as opposed to "matched on basis of isomorphism" ("structural").
  - chrisseaton 5y ago
    Right and you can’t match something by name if you can’t name it.
    - jhgb 5y ago
      That's not really true -- in structural typing, you can name things but the names themselves are just a convenience; an alias for something too long to type without getting lost in it.
      - chrisseaton 5y ago
        Well I don't know then. If you've got a better name for a type that you cannot express in the domain language but can be tracked by the compiler that'll be understandable in a public blog post then I'll use it?
        jhgb 5y ago
        Well...that's still just a type. I never found any reason to name it specially myself, even when I was thinking of similar things that are being described in the article (though not about Ruby, but rather about Lisp-y languages). Maybe I'm a bit influenced by the fact that there isn't such thing as "a type that you cannot express in the domain language" if you have SATISFIES (http://www.lispworks.com/documentation/HyperSpec/Body/t_satisf.htm http://www.lispworks.com/documentation/HyperSpec/Body/t_sati...), but still - a compiler can certainly synthesize "ad-hoc", unnamed types and perform reasoning with them.

by jhgb 5y ago

dmurray 5y ago

Well, at the very least, Ruby already has a type system so it's convenient to call these something different. And while you're correct that the stamps appear to be an alternative type system, for most people these types will be "unlike types you’ve usually worked with", because most people aren't heavily into Haskell or ML or other languages where it's natural to construct complex type systems like this.

lmm 5y ago
> And while you're correct that the stamps appear to be an alternative type system, for most people these types will be "unlike types you’ve usually worked with", because most people aren't heavily into Haskell or ML or other languages where it's natural to construct complex type systems like this. That ultimately causes more confusion though. These really are nothing more or less than types and you can do this kind of thing in a plain old type system and it's actually a lot easier and more effective. Maybe if enough people hear about types we can eventually drag programming culture kicking and screaming into the 1980s.

pugio 5y ago

Coming from traditional statically typed languages (Java, C++, Typescript, even Python or Ruby...), you might think of a type like "int" or "Float". He's calling stamps "micro-types" because they're more fine-grained than that. A stamp might tag a value as being between 0 and 255, for example, which is much more specific than "int". It would be really cool to work with a language that allows the user such fine-grained types, which is one reason I keep eyeing Idris.

jhgb 5y ago
> A stamp might tag a value as being between 0 and 255, for example, which is much more specific than "int". Yeah, that's a normal type. For example in Common Lisp, it's the type defined by the type specifier (INTEGER 0 255).
- chrisseaton 5y ago
  A simple range is one application you could use stamps for, but they can also represent that individual bits may or may not be set, or could even represent that individual bits are set with a given probability, which could inform scheduling decisions.
  - jhgb 5y ago
    Those things can in principle be expressed with a predicate using the SATISFIES type specifier, but the problem with that is that you currently can't pick such types apart for optimization purposes in any existing implementation, only test membership for values. Presumably that's one of the reasons why Qi/Shen was created.
brundolf 5y ago
TypeScript can... sort of do that. They could definitely take it further if they wanted to For example a type could be `0 | 1 | 2 | 3 | 4 | 5`, though there's no way right now to specify that as `0..5`
CorrectHorseBat 5y ago
Ada can do that

chrisseaton 5y ago

They’re non-nominal - you can’t name them in the language being compiled. They work at a finer level than the nominal system the programmer has access to. (I’m not a type theorist though.)

jhgb 5y ago
Hmm. I usually see "nominal" in this context as "matched on basis on type name", as opposed to "matched on basis of isomorphism" ("structural").
- chrisseaton 5y ago
  Right and you can’t match something by name if you can’t name it.
  - jhgb 5y ago
    That's not really true -- in structural typing, you can name things but the names themselves are just a convenience; an alias for something too long to type without getting lost in it.
    - chrisseaton 5y ago
      Well I don't know then. If you've got a better name for a type that you cannot express in the domain language but can be tracked by the compiler that'll be understandable in a public blog post then I'll use it?
      - jhgb 5y ago
        Well...that's still just a type. I never found any reason to name it specially myself, even when I was thinking of similar things that are being described in the article (though not about Ruby, but rather about Lisp-y languages). Maybe I'm a bit influenced by the fact that there isn't such thing as "a type that you cannot express in the domain language" if you have SATISFIES (http://www.lispworks.com/documentation/HyperSpec/Body/t_satisf.htm http://www.lispworks.com/documentation/HyperSpec/Body/t_sati...), but still - a compiler can certainly synthesize "ad-hoc", unnamed types and perform reasoning with them.