Hacker News new | past | comments | ask | show | jobs | submit login

> semantically inaccessible, not syntactically inaccessible.

You can give the semantics of everything that happens in a safe d-t language in terms of church encoded tag-value pairs and yet the programmer can't break the abstraction because abstraction-breaking operations are syntactically unavailable.

It should count as testament to the success of dynamic typing that the abstractions are so safely enforced that you can squint and suddenly the whole language is semantically founded on them.




> You can give the semantics of everything that happens in a safe d-t language in terms of church encoded tag-value pairs and yet the programmer can't break the abstraction because abstraction-breaking operations are syntactically unavailable.

This strikes me as just a Turing tarpit argument. Sure you can represent and enforce semantics syntactically, and you can probably also do this via automatic translations in many or most cases. Why is this compelling? And what does this have to do with types?

The definition of type system I gave is, "a syntactic method for enforcing levels of abstraction in programs". Ergo, not all syntactic methods qualify as a type system, but a specific kind of syntactic method classify type systems. Why do you think your translation qualifies?




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: