OCaml’s extensions are primarily it’s Module system (the m in it’s name), which allows for fun dynamic code generation entirely type safe. OCaml has others as well (row typing for record objects and such) but that is the primary big one that is unique among all HM languages (it’s module system is significantly more powerful than SML’s for example).
Elm’s main extension (really it’s only one I think) is it has some kind of ‘fake types’ that pretend to be typeclasses like number (matches both integers and float) and comparable (that matches a lot of stuff), however Elm does not do it in a type safe way and it’s extension to HM is entirely Unsound. For example Inferred type can be too generic with `number` and `Int` · Issue #1605 · elm/compiler · GitHub that allows you to basically ‘cast’ anything to anything (unsafely in a javascript context) by using them:
import Html
intId : Int -> Int
intId x = x
toInt x =
if x > 0
then intId x
else intId x
OCaml on the other hand is fairly rock solid for decades now, and any language features go through a bit of hell to get added and are only added if not emulatable in some other readable way and that it is entirely sound and so forth (Implicit Modules will be the next big language addition most likely, and it’s been years incoming).
Except it is not the source of the problem at all.
The problem are that even if you think about it, you have no control about who is going to use your API. You can make it the best ever, that will change nothing.
Plus… You can not escape the errors created by hardware or the layers behind you.
You are even a good example here. You think that a great argument for that type of type system is that they make you think about your input and output when this is far from being the root of the problem.
Maybe it is correct to say that strong typing allows you to be more explicit than weak typing in your APIs. This is for me personally the main reason I like working with strongly typed languages.
I completely agree with you, @DianaOlympos, that a typed system is not an adequate replacement for the fault-tolerant resilience that supervision tree-style concern segregation allows you to have.
Change what though? /me is confused about what is being discussed…
One big thing that it would change over unityping is that the contract that ‘my’ library gives to the user I can at least say that I will full-fill such-n-such contract and that the compiler makes certain that I do not do stupid crap like returning a value when I meant to return a {:ok, value} or so, it is meant to help me from making my mistakes. Sure you could type everything to take and return Dynamic types, but then I have to add typing tests to my tests in addition to testing the logic, which balloons them and may still not catch all cases that the compiler could do for me with ease.
Uh, I’m unsure what that has to do with a typing system? Static/Strong Typing vs Unityping should not depend on the hardware or anything else that exists beyond compile-time at all?
Root of what problem? The problem I’ve been speaking of is contractual and thinking about your inputs and outputs is the very essence of ensuring contracts at API bounds, not necessarily to verify the ‘user’ uses them as you state but that you yourself fullfills the contract that you state you are going to fullfill in a passing data sense, logical contracts are an entirely different issue (though typing can help with that as well, can prevent you from doing something stupid like multiplying a kilometer and a mile).
Very much this, the typing specifies a contract that I am promising to my users that I will fullfill (if I do not, it is a bug). How it is implemented internally is a separate matter, whether it is OOP, functional, stack calls, OpenCL, actor model, whatever, none of that has anything to do with typing.
I’m still confused about what is being talked about in regards to supervision tree concern segregation and what that has to do with static/strong typing vs unityping. ^.^;
How would you even apply such a thing to a static type system anyways? I think I need an example of that to understand what is being talked of… ^.^;
Why is Strong Typing better than Unityping? A simple example:
The 2nd argument to function `tbody` is causing a mismatch.
34| Table.tbody []
35|> [ List.map serpRow serp_list.entries ]
Function `tbody` is expecting the 2nd argument to be:
List (Table.Row msg)
But it is:
List (List (Table.Row msg))
It allow you to get rid of simple stupid bugs like this on a spot. With Unityping, you would get error at runtime at best scenario, at worst you’d get some garbage on screen or nothing at all and not a single hint what went wrong. Why don’t you get expected behaviour.
@OvermindDL1 I believe that @DianaOlympos’ statement was that using strong typing gives you a false sense of security, with security being defined as ‘being able to handle any failures’ (i.e. fault-tolerancy). (Note that I am paraphrasing here, so feel free to correct me, @DianaOlympos!)
I think this is unfair to Elm. I am a user for 4 years now (yikes) and haven’t run into thes issues. Do they exist, but do they impact my experience? No. Could they? Perhaps, but 4 years ain’t bad.
What I really wanted to understand, is how typeclasses feel (i.e. implicitness) in OCaml. How tricky can it get things to compile with a more complicated type system. What the impact of doing side-effect-y stuff is to type safe code - do you have the choice of using monads? I.e. can you solidify things, if you choose. If you want. How cryptic can compile errors get?
I.e. how tractable is OCaml, for a newb (i.e. me).
I remember getting really interested in OCaml 10 years ago (! I am getting old) but the focus on OO back then really put me off. I suspect that has changed for the better.
Overmind, strange to say, i am a big fan of yours, I love the indepthness, But sometimes you should perhaps focus on a bigger picture (obviously it is totally up to you, but this is a fan speaking ; )
Erlang style actor models / OTP etc. come into their own for hardware issues. One machine in a network goes down? Supervisors to the rescue
Strong typing (aka Maths) can prove well formed output. I.e. i have a program with this type signature:
String -> Html
I can guarantee that whatever String the program receives I will have a Html as an output.
guarantee is a strong word. But this is maths. Many people arent used to this type of power, so they don’t fully believe it.
However, if the machine which is running the code goes down, by all means have OTP structures on other machines to elegantly pick things up - but having supervisors to catch crashes caused by software errors is a v poor alternative in comparison to a ‘100% Gauarantee’.
I am talking of the fact that in the grand scheme of things (ie the production and maintenance of a complex system, which is SocioTechnical and not only technical because… it is complex and we write it) the type of Strong Static typing given by a HN type system is amazing in term of making the software output the expected result.
But it is really bad for making the process work well, because it bring social problems. In particular a feeling of false safety “it compiled so it is going to work correctly”, that is really dangerous.
That feeling is unique to a developer. Some will have that false safety, others wont. I, coming from Ruby/Python background don’t have that feeling (an so I naturally assume there are more like me). What does strong typing in compiled languages gives me is the safety that If I try to consume in some function a type, that this function can’t get as an input, compiler will tell me I’m doing something wrong (it’s not saying that I’m doing anything right, mind that!). And because of that I’ll probably get rid of one class of bugs at compile and not at random after a bug report from QA (because I forgot to write a test… ). Not saying I’m surely will get rid of them, but that strong types are another place where they are checked.
If having strong types in compile time gives you some false safety, you will get that same false safety if you use weakly typed language, and write tests. This false safety is not a trait of type system, but of a human writing code.
I don’t see strong/static typing as ‘security’, I see it purely from a contractual standpoint, telling the compiler what I intend to do before I do it (thus double checking me, never hurts to have that) and forwarding the contract I specified to the users as well so they can trust it works as defined.
Handling failures and security and more has entirely nothing to do with if a language is typed or not. I think a statically typed language can help with all of that, but it is not required by any stretch.
I first encountered those issues by experiencing them first-hand. I personally have ran in to quite a variety of both typing and compiler generation bugs in Elm.
Typeclasses do not exist in OCaml. OCaml’s whole system tends to forgo ‘fluff’ on top of typed systems. You will not see operator-explosions like in Haskell, or 800 different typed extensions to add things that the type system cannot do like in Haskell (typeclasses is one), instead everything tries to be explicit. Even the upcoming Implicit Module’s can be performed entirely explicitly as it is defined in that spec (only things in immediate ‘implicit scope’ are eligible for implicit passing, unlike Haskell, which looks program-wide in any scope anywhere for typeclasses).
Overall OCaml is very user-friendly. Even the Elm’s ‘Readable and suggesting’ errors are from OCaml (it can often give you hints and sometimes even exact code to fix a bug, and the BetterErrors addon makes it even better).
Do note, OCaml is not fully strict like Haskell, it was not designed to be a research language, rather it was designed by businesses to Get Work Done, just like Erlang, so it is not always so pure as Haskell. Although it is an entirely immutable language in a strongly typed system like Haskell, it has ways to break out of it, just like Elixir/Erlang/Beam gives you, including even little fully typed mutable cells (literally, think a Cell from Rust for example). It is not something you ever really need to use nor should be used, but it is there if you need raw speed while it remains completely and fully typed and safe in that way. For the absolute extreme cases OCaml has the ability to break the type system via magic (that is it’s literal call), you should never use it, ever (it has it’s uses, but those are practically non-existent anymore as it’s type system can represent about everything you need now, unlike Haskell’s without extensions piled on extensions). A big bonus is the OCaml’s compiler, even heavily large and complex programs compile in mere seconds, fully optimized.
It has no focus on OOP. It’s Object system is a Row-Record Typing System, it is not Java-like classes by any stretch. It has it’s uses but almost no one uses it as you can do near everything in the main system unless you really really need row-polymorphism (I.E., almost never, not never, but almost never).
A comparison, Elm has no static records (it had no need to add it, Javascript cannot represent fully static records either with any efficiency above normal allocated prototypes), it has row-polymorphic records, which is like OCaml’s Objects. Row-polymorphic records have a speed cost over static records in native code, hence why OCaml has the difference, but row polymorphic records (objects) and normal static records in OCaml compile to the same code for Javascript.
Heh, thanks. ^.^
And yeah, I do try to focus on the big picture (I am primarily an INTJ, as my wife is as well), but I have a lot of INTP as well (my secondary type, which my wife does get bugged by sometimes…often, but focusing on details at times can be very beneficial ^.^).
Not just hardware, but threads as well. I’ve replicated the BEAM Actor model in C++ a decade ago (built on top of ASIO with everything asynchronous with a coroutine switch/case model) and it worked so fantastically!
Indeed, this is one of the reasons Multicore OCaml (some of the PR’s have already been brought to trunk whoooooo!) is built as it is. Multicore OCaml should be ‘finished’ and released in the next Major version and it is built to have no thread control at all, rather it just adds a set of ‘extension points’ into the language. You can define a fully cooperatively multithreaded system, pre-emptive system, greenthread system, actor model, whatever you can really think for multicore, it is being designed to support (just need someone to build whatever style they want on top of it then), it is utterly fantastic. This is also a prime example of why I really like the OCaml compiler and their group, they do not bring in something like, oh, std::thread like C++ does, rather it just brings in the absolute most basic to be able to implement any style, not just one specific given style, and to do it as absolutely efficiently as possible. The language grows slow, but it grows smart. It did not in it’s old days (a lot was oddly added like it was in Erlang (parametric modules)), and they learned from those experiences and for over a decade now have been careful about what is added, and it shows very well.
Seems not at all related to typing systems at all but rather system design, so I’m still confused at how it relates?
Typing does nothing of the sort, I can define this with ease in OCaml:
let (+) l r = l - r
And it will compile and run fine, just does the exact opposite that you expect. Typing systems (well refined and dependent typing can help with this) do not ensure your logic is correct, they just confirm that the data will be in a given format, no less. Whatever you store in that format is up to you, but it at least prevents you from, say, forgetting a List.flatten() so you end up returning a list(list(term())) instead of a list(term()) like you meant.
Ooo, not seen/heard that podcast, it is queued up.
Mirage is very cool, it is an OS kernel entirely built in OCaml, proven very safe, tiny, and fast (it is fantastic for memory constrained embedded devices).
Indeed. I quite often have code like:
type EscapedString = EscapedString of string
let escape_string str = Html.escape_string str
let print_to_template (EscapedString str) = Template.render(str)
Single ‘head’ sum types in OCaml are very common, their whole purpose is just to make sure that given data is processed before use, or in the right form, or so forth (like take type Meter = Meter of int for example).
It is to save me from myself. I cannot list the number of times that I passed in radians to a function that takes degrees in C++ before I made a (zero-cost whoo) wrapper type to wrap everything up in. They just help catch the stupid stuff at compile-time, and I always end up making a lot of little stupid mistakes like that. ^.^
Entirely agree. At the very least a static typing system saves you from writing a bulk of your tests, and combined with a property testing system (like QuickCheck) you have to specify almost nothing for it to ‘just work’, thus leaving you to test specific cases for your tests, which is substantially reduced code overall.
I may rely on 1 + 2 equalling 3 (though that thought can break with my above example, though a refined/dependently typed language would catch that bug, an HM language would not), but I certainly do not trust even my own logic in anything even marginally complex (which is anything that takes more than a half-second to understand in detail).
). Not saying I’m surely will get rid of them, but that strong types are another place where they are checked.
