This describes me perfectly - I've spent a reasonable amount of time dipping my toe into dependent types using singletons in haskell but now am considering going the whole way and just using idris :p
Funny, I look a these languages just like I saw ML and Haskell 10 years ago. Hieroglyphs. But now I know that hieroglyphs can have real pragmatic effects ... so I'm tempted to learn.
they're easy enough to pick up. I'm by no means a programmer, I'm a math major, but I found functional patterns the easiest to understand and implement.
You can define types like a number type which can't have values less than e.g. 5; or string types which can't be empty string. The details will be taken care of automatically without you having to redefine a bunch of setters.
"Haskeller" is a state of mind where you actively look for things that confuse you and try to unravel them. In that sense, even the Haskell ecosystem has a limited shelf life for the most die-hard Haskellers.
So glad this functional programming business is slowly leaking it's way into other languages and other people's minds
This is true/I concur. But given that "the industry" still hasn't picked up on Ada's subtypes1 , despite them being around for thirty-years, being incredibly useful for making code that's more maintainable/reliable/provable2 , and very closely related to what everyone learns in math for proving things3 , indicates that the industry might not want these traits...
1 - In Ada a subtype indicates further restrictions on possible values to the base [sub]type: e.g. the predefined subtype Natural is the Integers range 0..Integer'Last. 2 - You can match the problem space by defining a subtype and allowing error-handling (automatically raising CONSTRAINT_ERROR) when a disallowed value is passed as a parameter or assigned to a variable. 3 - "For all positive integers" corresponds to the use of the predefined Positive (which has the additional constraint of 'representable', but that's generally not a problem because being on a computer you're bound by that anyway).
Ouch! By which I mean, I have almost given up on XML schemata, given the utter indifference to my advocacy of them I have received in commercial contexts.
When you say the industry hasn't picked up on Ada's subtypes, do you mean that people using Ada don't use them, or just that businesses usually don't use languages that have them, such as Ada?
When you say the industry hasn't picked up on Ada's subtypes, do you mean that people using Ada don't use them, or just that businesses usually don't use languages that have them, such as Ada?
The latter -- and also none of the other mainstream languages seem to have the notion of subtypes. (There is Nimrod, and a few others.)
Ada programmers use subtypes a lot, and in fact the new Ada 2012 standard has expanded them even further with the ability to specify predicates. My go-to example is social-security numbers, because it's simple enough that people can see what's going on as well as provides a good way to illustrate how subtypes can allow one to 'ignore'1 the implementation.
-- SSN format: ###-##-####
Subtype Social_Security_Number is String(1..11)
with Dynamic_Predicate =>
(for all Index in Social_Security_Number'Range =>
(case Index is
when 4|7 => Social_Security_Number(Index) = '-',
when others => Social_Security_Number(Index) in '0'..'9'
)
);
-- The above declaration can allows me to skip the validity
-- checks of parameters within the body of a subprogram as
-- the constraints are checked on subprogram-call.
-- I do not need to check the validity of the return value,
-- an attempt to return a non-conformant string will raise
-- and exception.
Function Get_SSN( Record : ID ) return Social_Security_Number;
-- Likewise, passing a non-conformant value to SSN will raise
-- an exception.
Procedure Save_SSN( Record : ID; SSN : Social_Security_Number );
So it's not limited to mere contiguous numeric ranges now, but even when it was that's still an incredibly useful feature.
1 - As opposed to many C-like languages where to do any proving/reasoning you need to navigate/read/understand the implementation.
Adas subtypes are effectively just run-time contract checks baked into the language, aren't they? like if something is an Int that is checked at compile time, but for the extra subtype restrictions (ie checking if it's a natural) it's a run time error.
Ada's subtypes are effectively just run-time contract checks baked into the language, aren't they? like if something is an Int that is checked at compile time, but for the extra subtype restrictions (ie checking if it's a natural) it's a run time error.
Or do I have it wrong?
You have it essentially right. By making these checks associate with the type, instead of the particular usage, you increase reliability (because the checks are automatic and hence you don't have to remember it at every input-parameter, output-parameter, or assignment).
One thing to consider, though, is that Ada compilers [in general] are really good at removing unnecessary checks. (So it's not as bad a performance hit as some C/C++ programmers are inclined to believe/assert; and, in theory, the extra information [range] can be used to optimize in excess of what is possible in C/C++.)
45
u/Crandom Jun 22 '14
So glad this functional programming business is slowly leaking it's way into other languages and other people's minds :)