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

Formalism aside, it seems like it's most useful in practice to think of type as defining what can be done with a value. The sidesteps the idea of type being something permanent and inherent to a value. In practice, the type might be metadata discoverable and actionable at run-time, it might be something that exists at compile-time to determine correctness of a program (based on how values are used), or both.

Does this point of view leave out anything crucial?




> Formalism aside, it seems like it's most useful in practice to think of type as defining what can be done with a value.

That might be a simpler way of explaining it, since "proposition" is rather abstract. Or perhaps, a type defines the valid state transitions your program can undergo at any given point, ie. given the data in your program (the program state S0), the types of all of that data define a set of valid transitions to another data set (program state S1).




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

Search: