4 ms·

This got me thinking, and I'm curious what a language would look like if basic types weren't directly usable. In other words, maybe type checking doesn't go fa

This got me thinking, and I'm curious what a language would look like if basic types weren't directly usable. In other words, maybe type checking doesn't go far enough: checking that I'm getting an int is less valuable than checking that I'm getting the right sort of data for the domain.

daxfohl 8y ago
unsigned int?
tzahola 8y ago
See Boost.Units: https://www.boost.org/doc/libs/1_65_0/doc/html/boost_units.html https://www.boost.org/doc/libs/1_65_0/doc/html/boost_units.h... It enforces correct units/dimensions at compile time, so you won’t be able to mix up length with time or area, etc.
ghayes 8y ago
This might be a good time to check out algebraic data types, esp. with a single constructor. For example, in Elm you might declare: type Length = Inches Int Then any function that accepts a Length, you can only pass in a length. This effectively acts like tagged tuples verified at compile time. You can later extend this type to be: type Length = Inches Int | Meters Int and any code that reads length would have to handle both cases (also checked at compile that). I have found this to be a great way of ensuring all of your types are correct (and sometimes, a great frustration of wishing I didn't have to wrap/unwrap types so often).
- GavinMcG 8y ago
  Yeah, that's one of my favorite takeaways from Elm. I'm thinking of it in an OO style, where perhaps instead of wrapping/unwrapping you're specifying an analog to object properties.
- insulanian 8y ago
  F# has units of measure [1], which are very nice for such a case you're describing. [1] https://fsharpforfunandprofit.com/posts/units-of-measure/ https://fsharpforfunandprofit.com/posts/units-of-measure/
usrusr 8y ago
Whenever I play with that idea in my head I get hung up on the question wether one could go even further down that road and drop variable names as a concept separate from types. If you already have a Surname instead of a String and a Birthday instead of a Date, why duplicate that into surname and bday? In a way, variable names are a bit like informal domain subtypes. Could we make them formal? I'm really not sure if that could be in any way practical at all, but I like the idea.
- andrewflnr 8y ago
  There is/was a programming language called Wake that used this idea. The supposed domain is down right now, so this documentation source code is the best reference I can find in a few minutes: https://github.com/MichaelRFairhurst/wake-compiler-docs/blob/master/faq.html#L45 https://github.com/MichaelRFairhurst/wake-compiler-docs/blob...
- GavinMcG 8y ago
  That's where my mind was headed as well. You'd still want variables for passing around instances (in a general sense; not specifically an OO sense) but everything else could be defined on the type. Sort of a types-as-classes approach.
- rbonvall 8y ago
  In some languages you don't give field names, just types. You bind fields to names only when pattern matching. For example in Haskell: type Year = Int type Month = Int type Day = Int -- fields have no names, just types data Date = Date Year Month Day -- we bind fields to names only when necessary next (Date y 12 31) = Date (y + 1) 1 1 next (Date y m d) | d == daysOf m = Date y (m + 1) 1 | otherwise = Date y m (d + 1) where daysOf = (!!) [0, 31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31] Is something like this what you mean?
  - usrusr 8y ago
    Thank you, good to know. Maybe those who don't know Haskell are doomed to reinvent isolated parts of it.
JoshTriplett 8y ago
If you did that, in what language would you write the validation code to check if you have a value in the correct domain, or convert between domains?
GavinMcG 8y ago
I think this post [0] points out how Haskell can implement this sort of thing, using DataKinds, and GeneralizedNewTypeDeriving with StandaloneDeriving. [0] https://lexi-lambda.github.io/blog/2016/06/12/four-months-with-haskell/ https://lexi-lambda.github.io/blog/2016/06/12/four-months-wi...

daxfohl 8y ago

unsigned int?

tzahola 8y ago

See Boost.Units: https://www.boost.org/doc/libs/1_65_0/doc/html/boost_units.html https://www.boost.org/doc/libs/1_65_0/doc/html/boost_units.h... It enforces correct units/dimensions at compile time, so you won’t be able to mix up length with time or area, etc.

ghayes 8y ago

This might be a good time to check out algebraic data types, esp. with a single constructor. For example, in Elm you might declare: type Length = Inches Int Then any function that accepts a Length, you can only pass in a length. This effectively acts like tagged tuples verified at compile time. You can later extend this type to be: type Length = Inches Int | Meters Int and any code that reads length would have to handle both cases (also checked at compile that). I have found this to be a great way of ensuring all of your types are correct (and sometimes, a great frustration of wishing I didn't have to wrap/unwrap types so often).

GavinMcG 8y ago
Yeah, that's one of my favorite takeaways from Elm. I'm thinking of it in an OO style, where perhaps instead of wrapping/unwrapping you're specifying an analog to object properties.
insulanian 8y ago
F# has units of measure [1], which are very nice for such a case you're describing. [1] https://fsharpforfunandprofit.com/posts/units-of-measure/ https://fsharpforfunandprofit.com/posts/units-of-measure/

usrusr 8y ago

Whenever I play with that idea in my head I get hung up on the question wether one could go even further down that road and drop variable names as a concept separate from types. If you already have a Surname instead of a String and a Birthday instead of a Date, why duplicate that into surname and bday? In a way, variable names are a bit like informal domain subtypes. Could we make them formal? I'm really not sure if that could be in any way practical at all, but I like the idea.

andrewflnr 8y ago
There is/was a programming language called Wake that used this idea. The supposed domain is down right now, so this documentation source code is the best reference I can find in a few minutes: https://github.com/MichaelRFairhurst/wake-compiler-docs/blob/master/faq.html#L45 https://github.com/MichaelRFairhurst/wake-compiler-docs/blob...
GavinMcG 8y ago
That's where my mind was headed as well. You'd still want variables for passing around instances (in a general sense; not specifically an OO sense) but everything else could be defined on the type. Sort of a types-as-classes approach.
rbonvall 8y ago
In some languages you don't give field names, just types. You bind fields to names only when pattern matching. For example in Haskell: type Year = Int type Month = Int type Day = Int -- fields have no names, just types data Date = Date Year Month Day -- we bind fields to names only when necessary next (Date y 12 31) = Date (y + 1) 1 1 next (Date y m d) | d == daysOf m = Date y (m + 1) 1 | otherwise = Date y m (d + 1) where daysOf = (!!) [0, 31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31] Is something like this what you mean?
- usrusr 8y ago
  Thank you, good to know. Maybe those who don't know Haskell are doomed to reinvent isolated parts of it.

JoshTriplett 8y ago

If you did that, in what language would you write the validation code to check if you have a value in the correct domain, or convert between domains?

GavinMcG 8y ago

I think this post [0] points out how Haskell can implement this sort of thing, using DataKinds, and GeneralizedNewTypeDeriving with StandaloneDeriving. [0] https://lexi-lambda.github.io/blog/2016/06/12/four-months-with-haskell/ https://lexi-lambda.github.io/blog/2016/06/12/four-months-wi...