Introduction to Functional Programming in OCaml(fun-mooc.fr)
fun-mooc.fr
Introduction to Functional Programming in OCaml
https://www.fun-mooc.fr/courses/parisdiderot/56002S02/session02/about
84 comments
Some note: compared to the Haskell mooc, the FUN ocaml mooc is quite pragmatic, they don't go into faux monadic concurrency through Continuations or Tree Functors. There are some mind bending exercices though. (speaking from the previous run of course)
I'm really interested in OCaml, especially now that Reason has reduced the entry barrier for our team, and the BuckleScript OCaml-to-JS compiler has matured.
A very pragmatic yet functional stack could show from this, call it the ORBS-stack (OCaml/Reason/BuckleScript).
Now I wonder what cool front-end frameworks, possibly binding to JS frameworks, exist. In PureScript I really like Thermite and Halogen.
A very pragmatic yet functional stack could show from this, call it the ORBS-stack (OCaml/Reason/BuckleScript).
Now I wonder what cool front-end frameworks, possibly binding to JS frameworks, exist. In PureScript I really like Thermite and Halogen.
I'm with you but the F#-Websharper stack already exists for isomorphic ML coding in both the front and backends. Reason/bucklescript is only on the frontend and is an entirely different "dialect" compared to OCaml.
Having both Ocaml and F# descending from ML doesn't say much really, other than both implementing Hindley–Milner type inference and sharing some syntax. They are very different languages.
For example Ocaml has functors, polymorphic variants and row polymorphism, versus F# which has .NET"s OOP and subtyping. F# as a language feels to me more limiting.
I won't comment on the runtimes / environments, as they have pros and cons, but there's something odd about F# to Javascript compilers. There's WebSharper and FunScript and now Fable. I don't understand why the community can't get behind a single one, because neither of them is popular enough to have reached critical mass. Take a look at WebSharper's commit activity for the past year and compare with Scala.js or with ClojureScript. And note I'm not saying anything about its technical merits.
Whereas for FunScript and Fable, well FunScript is probably going to die and neither of them seem to cope with "isomorphic" libraries.
For example Ocaml has functors, polymorphic variants and row polymorphism, versus F# which has .NET"s OOP and subtyping. F# as a language feels to me more limiting.
I won't comment on the runtimes / environments, as they have pros and cons, but there's something odd about F# to Javascript compilers. There's WebSharper and FunScript and now Fable. I don't understand why the community can't get behind a single one, because neither of them is popular enough to have reached critical mass. Take a look at WebSharper's commit activity for the past year and compare with Scala.js or with ClojureScript. And note I'm not saying anything about its technical merits.
Whereas for FunScript and Fable, well FunScript is probably going to die and neither of them seem to cope with "isomorphic" libraries.
There's more to F# then HM type inference plus ".NET's OOP and subtyping". OOP and subtyping are rarely used. While it lacks some of OCaml's powerful features it shares many core features such as algebraic data types, exhaustive pattern matching, immutability by default, Option types and so on. It's also arguably easier to read with it's white space significance and not needing the rather distracting "in" keyword.
Having the vast .NET library is a big plus for the language, of which OCaml has no equivalent. Other great features of F# are type providers, straightforward multi-core programming and units of measure, which I don't believe have OCaml equivalents.
Having the vast .NET library is a big plus for the language, of which OCaml has no equivalent. Other great features of F# are type providers, straightforward multi-core programming and units of measure, which I don't believe have OCaml equivalents.
I got exited about OCaml when I tried to solve my performance issues in Python, but then realised OCaml didn't have a good multi core story either...
Any progress in that area?
Given that rust has picked up a lot in terms of typing and even syntax from OCaml, is OCaml still worth investigating?
Any progress in that area?
Given that rust has picked up a lot in terms of typing and even syntax from OCaml, is OCaml still worth investigating?
Rust took affine substructural types and integrated them into a language that looks as similar to C and C++ as possible, to make it not seem foreign to your average programmer. You can think of Rust as a focused version of ATS2 with less features for practical reasons.
Rust is for building lower-level code which you would have written in C or C++ before. The comfort features and type system plus compiler support make it more amenable to writing application code as well, which would have been written in Java, C++ or Python out of comfort, so it's used for that, too.
OCaml is still relevant and they complement each other. Rust is decidedly not a functional programming language, so its type system isn't going to magically support expressing the kind of constraints and abstractions (for more maintainable and less bug-prone code) you're able to in OCaml, Haskell, or even ATS2. It's not Rust vs OCaml but Rust and OCaml.
The selling point of Rust over ATS2 or OCaml is the popularity and resulting ecosystem around it, just like the JVM.
OCaml's existing multicore story is practical with async and friends, but they're about to land the low-level framework that allows one to build various concurrency abstractions on top. That one's based on KC's research and is pretty cool, actually.
Rust is for building lower-level code which you would have written in C or C++ before. The comfort features and type system plus compiler support make it more amenable to writing application code as well, which would have been written in Java, C++ or Python out of comfort, so it's used for that, too.
OCaml is still relevant and they complement each other. Rust is decidedly not a functional programming language, so its type system isn't going to magically support expressing the kind of constraints and abstractions (for more maintainable and less bug-prone code) you're able to in OCaml, Haskell, or even ATS2. It's not Rust vs OCaml but Rust and OCaml.
The selling point of Rust over ATS2 or OCaml is the popularity and resulting ecosystem around it, just like the JVM.
OCaml's existing multicore story is practical with async and friends, but they're about to land the low-level framework that allows one to build various concurrency abstractions on top. That one's based on KC's research and is pretty cool, actually.
async is for concurrent I/O, not parallel processing.
I don't know about ocaml, but in general async is also about parallelism as it exposes concurrency opportunities. See cilk spawn for example.
Parallelism and concurrency are fundamentally different things. Parallelism is running independent computations simultaneously. Concurrency control is managing the use of shared resources by temporarily granting exclusive access to them to individual computations.
Imperative languages tend to blur the distinction between parallelism and concurrency, because the global state of a process by itself can be considered a shared resource. But in functional languages, it's natural to expect a sharper distinction: Because most data structures are logically immutable, the primary use for concurrency control is managing the interaction between the program and the “outside world”. On the other hand, parallelism is a powerful tool for speeding up the program's own internal calculations, even when no interaction with the “outside world” is involved.
Imperative languages tend to blur the distinction between parallelism and concurrency, because the global state of a process by itself can be considered a shared resource. But in functional languages, it's natural to expect a sharper distinction: Because most data structures are logically immutable, the primary use for concurrency control is managing the interaction between the program and the “outside world”. On the other hand, parallelism is a powerful tool for speeding up the program's own internal calculations, even when no interaction with the “outside world” is involved.
Concurrency is a property of the software (i.e. the problem domain): i.e. having multiple independent control flows. Parallelism is a property of the hardware, i.e. having the capability of running multiple operations (be it pure computation, memory access or IO).
To make use of parallel hardware you need concurrent software. Async is a way of exposing additional concurrency, thus enabling parallelism, to the hardware.
To make use of parallel hardware you need concurrent software. Async is a way of exposing additional concurrency, thus enabling parallelism, to the hardware.
> Parallelism is a property of the hardware, i.e. having the capability of running multiple operations (be it pure computation, memory access or IO).
Parallelism is a property of the program too: if it doesn't have independent subcomputations, the program is going to run sequentially even in hardware that supports parallelism.
> To make use of parallel hardware you need concurrent software.
Parallel Haskell shows otherwise.
Parallelism is a property of the program too: if it doesn't have independent subcomputations, the program is going to run sequentially even in hardware that supports parallelism.
> To make use of parallel hardware you need concurrent software.
Parallel Haskell shows otherwise.
>if it doesn't have independent subcomputations, the program is going to be run sequentially even in hardware that supports parallelism.
the property of having independent sub-computations is called concurrency.
the property of having independent sub-computations is called concurrency.
> the property of having independent sub-computations is called concurrency.
Nope. If I have two n-dimensional vectors, and want to compute their sum, there's no concurrency whatsoever: there's just n independent computations (each scalar sum). A pure parallelism problem.
(Well, there is a concurrency problem at a lower level of abstraction, if you want to schedule these computations over less than n processors. That's because the processors are shared resources that require temporary exclusive access to be used.)
References:
(0) https://existentialtype.wordpress.com/2011/03/17/parallelism...
(1) https://existentialtype.wordpress.com/2014/04/09/parallelism...
Nope. If I have two n-dimensional vectors, and want to compute their sum, there's no concurrency whatsoever: there's just n independent computations (each scalar sum). A pure parallelism problem.
(Well, there is a concurrency problem at a lower level of abstraction, if you want to schedule these computations over less than n processors. That's because the processors are shared resources that require temporary exclusive access to be used.)
References:
(0) https://existentialtype.wordpress.com/2011/03/17/parallelism...
(1) https://existentialtype.wordpress.com/2014/04/09/parallelism...
I see your blog article and raise a wikipedia [1]:
"In computer science, concurrency is the decomposability property of a program, algorithm, or problem into order-independent or partially-ordered components or units. This means that even if the concurrent units of the program, algorithm, or problem are executed out-of-order or in partial order, the final outcome will remain the same. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems."
Note the 'decomposability' part, i.e. the having the property of being decomposable.
[1] https://en.wikipedia.org/wiki/Concurrency_%28computer_scienc...
"In computer science, concurrency is the decomposability property of a program, algorithm, or problem into order-independent or partially-ordered components or units. This means that even if the concurrent units of the program, algorithm, or problem are executed out-of-order or in partial order, the final outcome will remain the same. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems."
Note the 'decomposability' part, i.e. the having the property of being decomposable.
[1] https://en.wikipedia.org/wiki/Concurrency_%28computer_scienc...
Zeroth, I'm not the owner of that blog. He's a CS researcher, I'm just a lowly programmer in the trenches. Just wanted to make that clear.
First, the Wikipedia article you quote is partially incorrect:
> This means that even if the concurrent units of the program, algorithm, or problem are executed out-of-order or in partial order, the final outcome will remain the same.
This is not true. Consider the following example: Mr. Foo and Ms. Bar are happily married, and own a shared bank account, whose initial balance is $400. Concurrently, they attempt to withdraw $200 and $300 respectively. The scheduling of the withdrawal operations will determine the final result:
(0) Foo has $200, Bar has nothing, and the final account balance is $200.
(1) Foo has nothing, Bar has $300, and the final account balance is $100.
> Note the 'decomposability' part, i.e. the having the property of being decomposable.
Both parallelism and concurrency are about decomposition. They are different kinds of decomposition, though. Parallel tasks cooperate towards a common goal. Concurrent tasks compete for access to common resources.
First, the Wikipedia article you quote is partially incorrect:
> This means that even if the concurrent units of the program, algorithm, or problem are executed out-of-order or in partial order, the final outcome will remain the same.
This is not true. Consider the following example: Mr. Foo and Ms. Bar are happily married, and own a shared bank account, whose initial balance is $400. Concurrently, they attempt to withdraw $200 and $300 respectively. The scheduling of the withdrawal operations will determine the final result:
(0) Foo has $200, Bar has nothing, and the final account balance is $200.
(1) Foo has nothing, Bar has $300, and the final account balance is $100.
> Note the 'decomposability' part, i.e. the having the property of being decomposable.
Both parallelism and concurrency are about decomposition. They are different kinds of decomposition, though. Parallel tasks cooperate towards a common goal. Concurrent tasks compete for access to common resources.
I think that Wikipedia claim is predicated on 'same result' for originally partially ordered results. Even a sequential implementation can produce different results if the requests arrive in different order.
> Parallel tasks cooperate towards a common goal. Concurrent tasks compete for access to common resources.
This definition is interesting, but I think it lack descriptive power: are web server tasks parallel as they are all contributing at fulfilling the incoming client request queue? Are threads of a matrix multiplication process concurrent as they compete for access to the cpu?
It also misses the whole reason for parallelism which is speed-up (by a constant) of execution.
Anyway, to go full circle, I stand by my assertion that async can be all about parallelism.
[BTW, this has been a great conversation, sometimes one need to put their thought in writing to actually fully understand them]
> Parallel tasks cooperate towards a common goal. Concurrent tasks compete for access to common resources.
This definition is interesting, but I think it lack descriptive power: are web server tasks parallel as they are all contributing at fulfilling the incoming client request queue? Are threads of a matrix multiplication process concurrent as they compete for access to the cpu?
It also misses the whole reason for parallelism which is speed-up (by a constant) of execution.
Anyway, to go full circle, I stand by my assertion that async can be all about parallelism.
[BTW, this has been a great conversation, sometimes one need to put their thought in writing to actually fully understand them]
Is ATS used at all outside academia?
yeah, here are some good posts on using ATS2 for internet-of-things applications
http://metasepi.org/en/tags/ats.html
http://metasepi.org/en/tags/ats.html
If you're looking for exhausting your CPU cores, you can do it with Python as well, by using multiple processes, like when using "multiprocessing". What Python and (currently) Ocaml won't do is being able to run in parallel multiple OS-managed threads that share the same address space. The approach in Ocaml is thus to use multiple processes instead of threads and do message passing between them and if you need to share some memory, you can do that too, although it gets tricky.
In terms of performance, inability to do in-process threads-based parallelism isn't Python's biggest problem though. Good throughput is generally achieved by avoiding indirection and by being able to control the memory layout. Because Ocaml is static, because Ocaml code isn't heavy on OOP and because Ocaml also gives you low level tools allowing you to control the memory layout, you can have code that's "as fast as C".
> Given that rust has picked up a lot in terms of typing and even syntax from OCaml, is OCaml still worth investigating?
Rust and Ocaml are very different programming languages. Rust does not have a GC and that changes its nature completely. For example Rust could be used for real-time systems where garbage collected languages would struggle. Another consequence for example is that Rust isn't a functional programming language.
In terms of performance, inability to do in-process threads-based parallelism isn't Python's biggest problem though. Good throughput is generally achieved by avoiding indirection and by being able to control the memory layout. Because Ocaml is static, because Ocaml code isn't heavy on OOP and because Ocaml also gives you low level tools allowing you to control the memory layout, you can have code that's "as fast as C".
> Given that rust has picked up a lot in terms of typing and even syntax from OCaml, is OCaml still worth investigating?
Rust and Ocaml are very different programming languages. Rust does not have a GC and that changes its nature completely. For example Rust could be used for real-time systems where garbage collected languages would struggle. Another consequence for example is that Rust isn't a functional programming language.
> If you're looking for exhausting your CPU cores, you can do it with Python as well, by using multiple processes, like when using "multiprocessing".
Successful multiprocessing frameworks are, in a modern sense, indistinguishable from networked peer-to-peer systems. While this space is well explored, it's very difficult to call the resulting discipline "easy." Just like threaded programming, it's easy to make something subtly wrong.
> Rust and Ocaml are very different programming languages. Rust does not have a GC and that changes its nature completely. For example Rust could be used for real-time systems where garbage collected languages would struggle.
Surveying the field, real time garbage collection is not a pipe dream. It's a delivered and purchasable reality. Propagating the myth that only direct memory management can possibly deliver good results is ignoring the last 15 years of hard work on the subject, as well as products in the field.
You're propagating a sort of urban legend. Please reconsider it.
Successful multiprocessing frameworks are, in a modern sense, indistinguishable from networked peer-to-peer systems. While this space is well explored, it's very difficult to call the resulting discipline "easy." Just like threaded programming, it's easy to make something subtly wrong.
> Rust and Ocaml are very different programming languages. Rust does not have a GC and that changes its nature completely. For example Rust could be used for real-time systems where garbage collected languages would struggle.
Surveying the field, real time garbage collection is not a pipe dream. It's a delivered and purchasable reality. Propagating the myth that only direct memory management can possibly deliver good results is ignoring the last 15 years of hard work on the subject, as well as products in the field.
You're propagating a sort of urban legend. Please reconsider it.
> Surveying the field, real time garbage collection is not a pipe dream. It's a delivered and purchasable reality. Propagating the myth that only direct memory management can possibly deliver good results is ignoring the last 15 years of hard work on the subject, as well as products in the field.
Hardcoding the optimal resource reclamation strategy into your program will always be more efficient at runtime than not doing so. What “real-time” garbage collection gives you is only freedom from arbitrarily long pauses, not closeness to the optimal strategy. Furthermore, it doesn't come for free: it imposes some memory usage overhead. Finally, garbage collection simply can't handle resources that need to be reclaimed in a deterministic fashion, like file handles, GUI objects and network connections.
Hardcoding the optimal resource reclamation strategy into your program will always be more efficient at runtime than not doing so. What “real-time” garbage collection gives you is only freedom from arbitrarily long pauses, not closeness to the optimal strategy. Furthermore, it doesn't come for free: it imposes some memory usage overhead. Finally, garbage collection simply can't handle resources that need to be reclaimed in a deterministic fashion, like file handles, GUI objects and network connections.
> Hardcoding the optimal resource reclamation strategy into your program will always be more efficient at runtime than not doing so.
That depends on what you mean by efficient. Since this thread is about real-time stuff, you may be right (though I wouldn't be on it). However, often a GC will give better throughput.
It depends on the style of memory management on both sides, of course. But for example, in a situation where you call `free` (or, `delete`, etc.) to free each allocation, you might end up doing more work than a copying GC, where you only have to track live references.
That depends on what you mean by efficient. Since this thread is about real-time stuff, you may be right (though I wouldn't be on it). However, often a GC will give better throughput.
It depends on the style of memory management on both sides, of course. But for example, in a situation where you call `free` (or, `delete`, etc.) to free each allocation, you might end up doing more work than a copying GC, where you only have to track live references.
Of course, “the optimal resource reclamation strategy” depends on what you want to optimize in the first place. I didn't intend to suggest it's always “free every resource as soon as you don't need it anymore”.
Having worked with real-time systems, it's far from being an urban legend. Please name "real-time" garbage collectors available for mainstream languages.
And note that I'm not talking about ability to serve soft real-time services where you're allowed between 1 to 5% of all transactions to miss their deadline. Do that for a car break system or for an airplane guidance system and lives are lost. Heck, do that for video decoding and frames are dropped.
And note that I'm not talking about ability to serve soft real-time services where you're allowed between 1 to 5% of all transactions to miss their deadline. Do that for a car break system or for an airplane guidance system and lives are lost. Heck, do that for video decoding and frames are dropped.
They make new ones on a regular basis with different properties. Most customers just buy the existing products from the commercial sector, though. Here's a few links to performance and embedded-oriented ones that support predictable pause times with one letting it go down to one, move instruction given pauses are interruptable.
http://www.jopdesign.com/doc/nbgc.pdf
https://www.usenix.org/legacy/events/vee05/full_papers/p46-c...
http://www.cse.buffalo.edu/~lziarek/euro.pdf
http://www.aicas.com/papers/ismm02f-siebert.pdf
So, there's some examples to work with. There's plenty more, too. Just search Google with terms "concurrent," "real-time," and "GC." Or "pauseless" replacing "concurrent." Or "hard" before "real-time." That combo is how I track them.
http://www.jopdesign.com/doc/nbgc.pdf
https://www.usenix.org/legacy/events/vee05/full_papers/p46-c...
http://www.cse.buffalo.edu/~lziarek/euro.pdf
http://www.aicas.com/papers/ismm02f-siebert.pdf
So, there's some examples to work with. There's plenty more, too. Just search Google with terms "concurrent," "real-time," and "GC." Or "pauseless" replacing "concurrent." Or "hard" before "real-time." That combo is how I track them.
You can do functional programming without garbage collection. The problem is social: few people in the functional programming community are interested in substructural types.
Can you elaborate on how a FP language might be implemented without a garbage collector? How do things like closure/lambdas wok without GC? I tried to lookup "substructural types" but wasn't able to find anything.
I’m writing a functional language without a GC, so maybe I can offer some insight.
The basic reasons you want a GC are closures, as you mention, and reference cycles.
In a pure, eagerly evaluated language, cycles aren’t possible, so naïve reference-counting is enough to reclaim all garbage. If the language has mutable reference types, you can still use RC, but you need a cycle detector.
Closures are more interesting.
A neat thing about purely functional languages is that you can’t observe whether something is a value or a reference, so there’s no difference (apart from performance) between copying and sharing. Purely functional data structures take advantage of this to share common parts of modified structures. For instance, when replacing a node in a tree, you produce a new tree, but all nodes are shared except the O(log n) nodes in the path from the root to the new node.
What I do in my language project, then, is to always copy (or move) values into a closure. If they’re unboxed, they’re probably small, and if they’re boxed, they’re in a reference-counted or copy-on-write structure, so sharing is safe.
The next thing you can do is to unbox closures (like C++ lambdas). You only need to box them (like C++ std::function) if you want them to have uniform size, for example if you’re storing them in a homogeneous list.
Finally, you tie value lifetimes to scopes. When a value goes out of scope, you drop it and reclaim its memory immediately (or place it on a queue, for deferred RC). That’s where stack-based languages become really handy, part of the reason I’m writing one. That’s also where substructural types become interesting, because they let you encode the answer to the question “When am I allowed to copy or drop this value?”
Rust augments this with “lifetimes”, which are essentially a static approximation of stack depth. For instance, you can talk about references to objects on the stack, but you can’t store a reference to a younger value into an older value, because the younger one will be reclaimed first—its lifetime is not a supertype of the destination’s. This prevents the problem of dangling references.
I don’t feel like substructural types are really geared toward functional languages, however; where they really shine is safe imperative programming like Rust—for a particular definition of “safe”, anyway.
The basic reasons you want a GC are closures, as you mention, and reference cycles.
In a pure, eagerly evaluated language, cycles aren’t possible, so naïve reference-counting is enough to reclaim all garbage. If the language has mutable reference types, you can still use RC, but you need a cycle detector.
Closures are more interesting.
A neat thing about purely functional languages is that you can’t observe whether something is a value or a reference, so there’s no difference (apart from performance) between copying and sharing. Purely functional data structures take advantage of this to share common parts of modified structures. For instance, when replacing a node in a tree, you produce a new tree, but all nodes are shared except the O(log n) nodes in the path from the root to the new node.
What I do in my language project, then, is to always copy (or move) values into a closure. If they’re unboxed, they’re probably small, and if they’re boxed, they’re in a reference-counted or copy-on-write structure, so sharing is safe.
The next thing you can do is to unbox closures (like C++ lambdas). You only need to box them (like C++ std::function) if you want them to have uniform size, for example if you’re storing them in a homogeneous list.
Finally, you tie value lifetimes to scopes. When a value goes out of scope, you drop it and reclaim its memory immediately (or place it on a queue, for deferred RC). That’s where stack-based languages become really handy, part of the reason I’m writing one. That’s also where substructural types become interesting, because they let you encode the answer to the question “When am I allowed to copy or drop this value?”
Rust augments this with “lifetimes”, which are essentially a static approximation of stack depth. For instance, you can talk about references to objects on the stack, but you can’t store a reference to a younger value into an older value, because the younger one will be reclaimed first—its lifetime is not a supertype of the destination’s. This prevents the problem of dangling references.
I don’t feel like substructural types are really geared toward functional languages, however; where they really shine is safe imperative programming like Rust—for a particular definition of “safe”, anyway.
Agree with most of this, and even upvoted it, but...
> I don’t feel like substructural types are really geared toward functional languages, however; where they really shine is safe imperative programming like Rust—for a particular definition of “safe”, anyway.
I disagree with this. Even vanilla Standard ML and Haskell can benefit from substructural types. The structural rules (weakening, contraction) don't have to be an all-or-nothing proposition. Why should I be forced to pick one between garbage collection for in-memory data structures (which Rust won't give me, at least not out of the box), and deterministic reclamation guarantees for file handles and network connections (which ML and Haskell won't give me)? I want both!
> I don’t feel like substructural types are really geared toward functional languages, however; where they really shine is safe imperative programming like Rust—for a particular definition of “safe”, anyway.
I disagree with this. Even vanilla Standard ML and Haskell can benefit from substructural types. The structural rules (weakening, contraction) don't have to be an all-or-nothing proposition. Why should I be forced to pick one between garbage collection for in-memory data structures (which Rust won't give me, at least not out of the box), and deterministic reclamation guarantees for file handles and network connections (which ML and Haskell won't give me)? I want both!
Thanks for your insight. This is all very interesting. I'm reading about lifetimes and static analysis now. I hope you let HN know about your language when its time. I will be very interested hear more considering what you mentioned the inspiration was.
You can check my profile for the GitHub repo; it’s a long work-in-progress research project, so I don’t like to advertise too much, but you can play around with the old compiler and check out the work on the new one if you’re interested.
> I tried to lookup "substructural types" but wasn't able to find anything.
A substructural type system lets you express constraints on how many times a value can be used. More precisely:
(0) An object of an affine type cannot be used more than once. This is enforced by not allowing the same object to exist in multiple environments. Affinely typed objects can be moved (in the Rust sense) from one environment to another, but as soon as this happens, the object ceases to exist in the original environment. Affinely typed objects can be reclaimed as soon as they are first used (since they can't be used again) or go out of scope (since no other scope has access to them), so no dynamic garbage collection is necessary for them.
(1) An object of a relevant type has to be used at least once. This is enforced by requiring the result of every computation to be fed into some other computation. In lazy languages, relevant types can be used for strictness optimizations: if the result of a computation is guaranteed to be used, then computing the result upfront eliminates the overhead of creating lazy suspensions.
(2) An object of a linear type has to be used exactly once. A linear type is just a type that is both affine and relevant, so everything mentioned above applies.
> How do things like closure/lambdas wok without GC?
A closure has its own environment. With affine types, when a closure captures an object from the outer context, the object ceases to exist in the outer environment. This is how move closures already work in Rust.
---
A digression: This is why I find GHC's plethora of type system extensions utterly disappointing. They marginally increase Haskell's expressiveness in areas where the language is already very expressive, but they don't address the language's limitations w.r.t. resource management. For instance, Haskell is incapable of statically enforcing that file handles won't leak.
A substructural type system lets you express constraints on how many times a value can be used. More precisely:
(0) An object of an affine type cannot be used more than once. This is enforced by not allowing the same object to exist in multiple environments. Affinely typed objects can be moved (in the Rust sense) from one environment to another, but as soon as this happens, the object ceases to exist in the original environment. Affinely typed objects can be reclaimed as soon as they are first used (since they can't be used again) or go out of scope (since no other scope has access to them), so no dynamic garbage collection is necessary for them.
(1) An object of a relevant type has to be used at least once. This is enforced by requiring the result of every computation to be fed into some other computation. In lazy languages, relevant types can be used for strictness optimizations: if the result of a computation is guaranteed to be used, then computing the result upfront eliminates the overhead of creating lazy suspensions.
(2) An object of a linear type has to be used exactly once. A linear type is just a type that is both affine and relevant, so everything mentioned above applies.
> How do things like closure/lambdas wok without GC?
A closure has its own environment. With affine types, when a closure captures an object from the outer context, the object ceases to exist in the outer environment. This is how move closures already work in Rust.
---
A digression: This is why I find GHC's plethora of type system extensions utterly disappointing. They marginally increase Haskell's expressiveness in areas where the language is already very expressive, but they don't address the language's limitations w.r.t. resource management. For instance, Haskell is incapable of statically enforcing that file handles won't leak.
Mathieu Boespflug is from what I understand working on bringing linear types to ghc: https://ghc.haskell.org/trac/ghc/wiki/LinearTypes and https://redd.it/50nkbo
Re: last part
Idris programming language has "Uniqueness types" [1], that are inspired by Clean and Rust.
There is also an interesting talk [2] where Idris author discusses state/side-effects management.
[1] http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...
[2] https://www.youtube.com/watch?v=kpPyolN65s0
Idris programming language has "Uniqueness types" [1], that are inspired by Clean and Rust.
There is also an interesting talk [2] where Idris author discusses state/side-effects management.
[1] http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...
[2] https://www.youtube.com/watch?v=kpPyolN65s0
Statements like this one worry me a lot:
> We also haven’t checked any of the metatheory, so this could all be fatally flawed!
What I think makes the most sense is to have a nested hierarchy of type universes:
(0) All types
(1) Types that support sharing (data structures, first-class functions, but not ephemeral resources)
(2) Types that support equality testing (data structures not containing first-class functions)
Standard ML already has a similar hierarchy, but levels (0) and (1) are collapsed into a single one. At least it is intuitively obvious that this isn't wrong. The type safety proofs can come later.
Also, I'd rather not have a notion of borrowing at all. It's fine for Rust, because it's a low-level language. But, in a high-level language, if you want to share data structures, just use garbage collection. And, if you really want to share mutable objects (which most of the time you shouldn't), use mutexes. Mutexes themselves don't exactly support sharing, but they can be explicitly cloned and locked.
> We also haven’t checked any of the metatheory, so this could all be fatally flawed!
What I think makes the most sense is to have a nested hierarchy of type universes:
(0) All types
(1) Types that support sharing (data structures, first-class functions, but not ephemeral resources)
(2) Types that support equality testing (data structures not containing first-class functions)
Standard ML already has a similar hierarchy, but levels (0) and (1) are collapsed into a single one. At least it is intuitively obvious that this isn't wrong. The type safety proofs can come later.
Also, I'd rather not have a notion of borrowing at all. It's fine for Rust, because it's a low-level language. But, in a high-level language, if you want to share data structures, just use garbage collection. And, if you really want to share mutable objects (which most of the time you shouldn't), use mutexes. Mutexes themselves don't exactly support sharing, but they can be explicitly cloned and locked.
> For instance, Haskell is incapable of statically enforcing that file handles won't leak.
It is capable of it. You can do it with one monad transformer layer per file handle. Yes, that's utterly inconvenient, but you can do it. It would be far less inconvenient with (higher) row types.
It is capable of it. You can do it with one monad transformer layer per file handle. Yes, that's utterly inconvenient, but you can do it. It would be far less inconvenient with (higher) row types.
That forces you to deallocate resources in the inverse order of allocation, which may or may not be what you want. For example, the lock acquisition and release pattern used in the implementation of Lehman-Yao trees (and variants thereof) is inexpressible using monadic regions.
Hmm, well I've never implemented this myself so I'm not going to contradict you, but I'd be really surprised if you can't hoist into the monad transformer stack and close off a lower region earlier than the top-level region.
Would this be safe if the destructor of an inner region requires objects from outer regions to still exist?
I don't see how there could be any such requirements, if we're talking about file handles.
I'm pretty sure DBMS implementors have to work with data structures whose nodes are spread across several files, and which have to be locked and unlocked in very precise ways to preserve the integrity of the data they contain. I'd like to be able these locking and unlocking patterns with types.
[deleted]
Wow, thanks for the comprehensive answer. Its much appreciated.
The basic way to do it is just to allocate and delete things without the safety of a GC. ;) PreScheme did that among other things:
https://en.wikipedia.org/wiki/PreScheme
The medium approach might be using linear types like in ATS language:
http://www.ats-lang.org/
http://ats-lang.sourceforge.net/PAPER/LDD-plpv07.pdf
The heavyweight approach is integrating one with a theorem prover with C extraction like in COGENT:
https://ts.data61.csiro.au/projects/TS/cogent.pml
https://ts.data61.csiro.au/publications/nictaabstracts/8956....
Hope these give you ideas of how it can be done with what benefits and effort.
https://en.wikipedia.org/wiki/PreScheme
The medium approach might be using linear types like in ATS language:
http://www.ats-lang.org/
http://ats-lang.sourceforge.net/PAPER/LDD-plpv07.pdf
The heavyweight approach is integrating one with a theorem prover with C extraction like in COGENT:
https://ts.data61.csiro.au/projects/TS/cogent.pml
https://ts.data61.csiro.au/publications/nictaabstracts/8956....
Hope these give you ideas of how it can be done with what benefits and effort.
There's work on multicore doing on right now; IIRC, there was a possibility that it could've shipped in the 2015 December release, but didn't make it. So I think/hope it should be available in the near future.
Can't say I've tried it, but this approach looks very promising and has a nice, very composable API https://github.com/ocamllabs/reagents
Regarding Rust v OCaml, Rust is a nice language but solving a very different problem. The type system is far weaker than that of OCaml's, it's less expressive (more verbose) by virtue of its sometimes-GCless GC. Rust is meant for system programming, and OCaml is rather more general purpose and pleasant to write in, while remaining incredibly performant.
Regarding Rust v OCaml, Rust is a nice language but solving a very different problem. The type system is far weaker than that of OCaml's, it's less expressive (more verbose) by virtue of its sometimes-GCless GC. Rust is meant for system programming, and OCaml is rather more general purpose and pleasant to write in, while remaining incredibly performant.
OCaml is GCed and can infer more type annotations than Rust, so its code feels closer to Python.
Rust is best for complex systems where tight control of resources is required.
Rust is best for complex systems where tight control of resources is required.
Look at Erlang / Elixir for that specific feature.
The background soundtrack for the intro video sounds hilarious for some reason :)
Looks like a good course, will join.
Looks like a good course, will join.
Is knowledge of French required for following this course?
It's in English.
OK, cool. I just registered on fun-mooc.fr and saw they've got courses in French.
Disclosure : I'm French and know some people who dubbed the course.
The course may be taught in English but speakers are mostly French people. So expect crappy English accent.
The site itself is an attempt by the French government to build a French mooc platform.
The course may be taught in English but speakers are mostly French people. So expect crappy English accent.
The site itself is an attempt by the French government to build a French mooc platform.
The site was launched by the ministry of higher education and research of France, and there are mainly courses from French universities or research centers on it. Their first target is the countries where French is spoken (for instance, in West Africa) but the courses also try to have an English version.
I'm so excited and I just can't hide it! ;-)
Has this course changed or evolved in any way from the one that was given last year at this time (which was very good but had a few sizeable discreet jumps in the learning curve at certain points, which could have done with being smoothed out a little).
The overall structure stays the same, but we have made some changes: notably, we reduced the workload by suppressing some exercises which turned out to be too difficult, and quite a few glitches have been fixed.
If you have precise suggestions for improvement, please do not hesitate to send them to the course authors, there maight still be time to take them into account.
If you have precise suggestions for improvement, please do not hesitate to send them to the course authors, there maight still be time to take them into account.
Why OCaml instead of other functional languages such as Scala, Haskell, Erlang, etc...? Is there anything unique about OCaml.
A mother offered his son, on his birthday, two nice designer ties. Naturally, the son quickly took one of the two ties, put it on, and showed it smiling to his mother.
The mother, almost crying, asked "You dont like the other tie?"
The mother, almost crying, asked "You dont like the other tie?"
Because they are French ;) and Ocaml is as good as those you mentioned for teaching FP.
It is purer than Erlang, has less cruft than Scala, is more practical than Haskell, and in my opinion has a very nice syntax. It is also very fast.
>It is purer than Erlang
Not sure what value of 'pure' you are using here. Erlang has (practically) no mutation to speak of. Thus I would consider that purer.
Ocaml on the other hand is as mutating as you want it to be.
Not sure what value of 'pure' you are using here. Erlang has (practically) no mutation to speak of. Thus I would consider that purer.
Ocaml on the other hand is as mutating as you want it to be.
Yes I guess I was throwing static typing, somewhat incorrectly, into the "pure" catch-all.
I did this last year and don't remember much. What were the sizable discreet jumps?
I think some of the "question 3s" in the exercises were quite a challenge about 3 weeks into the course, and for people like me who insist on getting 100%, I remember spending 4-5x the allotted time on them (or maybe I'm just slow). But as per @ocamlmoocs comment here it looks like some of this has been looked at.
Sounds like a lot of fun! I'm a Clojure user feeling queasy about leaving s-expressions, but am very interested in the type safety. Signing up now...
I founded and help maintain a very large Clojure codebase and to be honest, I am sick to death of not having a real type system to help me.
Sure, we can test the crap out of our code watching for npe's. We can lint like crazy. We can write large integration tests to better understand the larger picture better. But ultimately nothing is as pervasive as the compiler relentlessly asking you to be clear.
What's more, the benefits of a language like OCaml (where Tagged unions, GADTs, direct modeling of errors via an Either composition, etc. rule the day) on your code leads you to a really good place when the codebase is sufficiently large.
Giving up s-expressions and monads is indeed a sad thing. I'd miss it.
Sure, we can test the crap out of our code watching for npe's. We can lint like crazy. We can write large integration tests to better understand the larger picture better. But ultimately nothing is as pervasive as the compiler relentlessly asking you to be clear.
What's more, the benefits of a language like OCaml (where Tagged unions, GADTs, direct modeling of errors via an Either composition, etc. rule the day) on your code leads you to a really good place when the codebase is sufficiently large.
Giving up s-expressions and monads is indeed a sad thing. I'd miss it.
You don't need to leave monads in OCaml (in fact, I'd be very sad to not be using them regularly). Typically the Lwt, Option, and Error monad. (Also speaking as a former Clojurer).
> I founded and help maintain a very large Clojure codebase and to be honest, I am sick to death of not having a real type system to help me.
What sort of size is the breaking point in your opinion?
I've recently made the move from f# to Clojure and I'm significantly more productive but I'm worried that when I get to larger projects (10-100kloc) I will come unstuck.
What sort of size is the breaking point in your opinion?
I've recently made the move from f# to Clojure and I'm significantly more productive but I'm worried that when I get to larger projects (10-100kloc) I will come unstuck.
It'd be much more fruitful to talk about this directly rather than via a forum where I am rate limited. :(
If you reach out to me via email you'll probably find me. You can find that email by searching for my username on the C2 wiki. Posting it here would be troublesome.
If you reach out to me via email you'll probably find me. You can find that email by searching for my username on the C2 wiki. Posting it here would be troublesome.
What about core.typed?
What about it?
I believe it qualifies as a "real type system", doesn't it?
Not really? We have a lot of options for opt-in run time verification, and then we can find new and interesting ways to break static verifiers with macros.
I don't mean to imply that core.tyoed is fictitious but I wouldn't consider it a substitute for real, pervasive static typing.
I don't mean to imply that core.tyoed is fictitious but I wouldn't consider it a substitute for real, pervasive static typing.
Read Real World OCaml and you'll find plenty use of S-Expressions for serialization and configuration due to Core libs by Jane Street :).
hey Jane Street!