Am 05.10.2018 um 12:49 schrieb Ivan Perez:

The design approach you're after is called "Capabilities". It's not ordinarily described as a type system, and I'm not sure whether it's a good idea to use static types in the first place because there are situations where you want to grant or revoke them dynamically.

In part, isn't specifying this up-front what iOS and Android do with permissions, or docker with capabilities?

Even these grant and revoke permissions based on user actions. What you can describe statically is right relationships - IF the user has given permission such-and-so, THEN this-and-that activity is allowed. Maybe that's the way to go. If not: Any alternative should have spent at least some thought about how to deal with rights being granted and revoked.

You'd probably want an ABI for types, no? You'd need a new executable format (among many other things!).

The question is: would it be worth it? Types are wonderful in Haskell because they allow us to structure our programs. What would structuring processes via types accomplish? It would improve the situation with shell scripting/pipes as you allude, but that's still an immense amount of effort.

Now that I think about it… having something like an ABI or a "Haskell binary format" with types in it might indeed be useful in more cases than this one. It seems when a Haskell projects gets a bit larger people tend to search for ways to make it more modular. They try plugin frameworks, OS-level dynamic linking, on-the-fly compilation etc. But I repeatedly get the feeling that all these current approaches aren't actually very good. But what if we had some kind of specialized format for compiled, dynamically loadable, typed Haskell libraries? Something between a plain OS library and bytecode. This might help make programs more modular while keeping them type safe. One thing that might be useful to add next would be some kind of centralized registry of types, so that a plugin/library could extend the ways the system could be extended. And going along this line of thought even further leads to… uhm… oh.    OH. Ok, so, it's the month of Halloween, right? Because… OSGi, but in Haskell. Well, maybe there's some sane point in between? Cheers, MarLinn

Am 05.10.2018 um 21:46 schrieb MarLinn:

It seems when a Haskell projects gets a bit larger people tend to search for ways to make it more modular. They try plugin frameworks, OS-level dynamic linking, on-the-fly compilation etc. But I repeatedly get the feeling that all these current approaches aren't actually very good. But what if we had some kind of specialized format for compiled, dynamically loadable, typed Haskell libraries? Something between a plain OS library and bytecode. This might help make programs more modular while keeping them type safe.

I've been believing that having a strict, universally-understood binary format was the one thing that enabled Java's library ecosystem. Which is huge, with a constant evolution of new generations and survival of the fittest. The downside is that compatibility with an established binary format is a pretty restricting design constraint on language evolution - you cannot evolve the language in ways that require a change to the binary format, unless you are willing to give up compatibility with all the precompiled binaries that are around. I think it's doable, if the binary format has been carefully designed to allow the kind of extensions that are being tought about. The other prerequisite is that if a change to the binary format is unavoidable, old formats stay readable. I.e. the loader needs to be able to read old format, indefinitely. Alternatively, code repositories could convert the code at upload time - the compatibility code would then live in the repositories and not in the loader (which makes the code harder to write but keeps the runtime smaller). Well, that's what I can say from the Java and repository perspective. I'm pretty sure there are other, and more important perspectives :-) Regards, JO

I sort of see why you might now, but I'm not sure it's what you mean? Could you elaborate? I think you can if you base this in some sort of indexed monad and have a way to join indices. Your process then become a -> (ioM e) a, where e is the neutral element or index for the index join operation. Perhaps indices could denote sets of permissions or capabilities. Ivan On Fri, 5 Oct 2018 at 22:09, Vanessa McHale wrote:

Another thing that would be different in the OS case would likely be that one could not have programs/processes of type

a -> a

...which would make any types stored in an ABI a good deal less flexible than those in Haskell.

On 10/05/2018 02:46 PM, MarLinn wrote:

...

...

You'd probably want an ABI for types, no? You'd need a new executable format (among many other things!).

The question is: would it be worth it? Types are wonderful in Haskell because they allow us to structure our programs. What would structuring processes via types accomplish? It would improve the situation with shell scripting/pipes as you allude, but that's still an immense amount of effort.

Now that I think about it… having something like an ABI or a "Haskell binary format" with types in it might indeed be useful in more cases than this one.

It seems when a Haskell projects gets a bit larger people tend to search for ways to make it more modular. They try plugin frameworks, OS-level dynamic linking, on-the-fly compilation etc. But I repeatedly get the feeling that all these current approaches aren't actually very good. But what if we had some kind of specialized format for compiled, dynamically loadable, typed Haskell libraries? Something between a plain OS library and bytecode. This might help make programs more modular while keeping them type safe.

One thing that might be useful to add next would be some kind of centralized registry of types, so that a plugin/library could extend the ways the system could be extended.

And going along this line of thought even further leads to… uhm… oh. OH.

Ok, so, it's the month of Halloween, right?

Because… OSGi, but in Haskell.

Well, maybe there's some sane point in between?

Cheers, MarLinn

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

There's a lot of other stuff going on too, not just binary sizes - GHC's runtime, a dynamic memory allocator, etc. I would hesitate to use Haskell in the embedded context or for hardware-level stuff. I presume GHC's approach to laziness has a role in this. I don't have much experience with OCaml but my experience with ATS is that it's very much possible to have functional, ML-style programming without a runtime or even dynamic memory allocation. On 10/19/18 4:02 PM, Andreas Reuleaux wrote:

While this may not be an answer to your specific question, you may want to have a look at MirageOS, the Operating System written in Ocaml by Anil Madhavapeddy el., https://mirage.io/

We had discussed this some while ago in our seminar, and I learned that Ocaml may be a better fit for writing an operating system than Haskell, due to Ocaml's ability to produce small binaries, smaller than Haskell binaries in any case usually. - Being involved with Haskell personally, I would like to be proven wrong, of course (ie. I would like to see small Haskell binaries), and I have heard of some former efforts of writing an OS in Haskell as well (but I would have to search for links).

just my 2 cents, Andreas

Yotam Ohad writes:

...

Hi, In the last couple of days, I've been toying with the thought of an operating system in which programs (or more accurately, any process) has a distinct type which limits its use of the machine. For example, `echo` (String -> String) won't be able to print an output without a second program which would handle changing stdout.

I think it could "break down" the IO monad into other structures that are better at specifying what is changing: A file is read / memory written / etc. I do, however, not sure how to incorporate drivers (which handles IO and external devices) into this. Giving them an `IO a` type feels like cheating. I would be much cooler if there was a way to treat them like the `echo` function from earlier.

What are your thoughts/suggestions? I'll be happy to hear them.

Yotam _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

---

Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

On Oct 20, 2018, at 09:11, Vanessa McHale wrote: I would hesitate to use Haskell in the embedded context or for hardware-level stuff. I presume GHC's approach to laziness has a role in this.

There’s a bit of a complication here. It’s true that standard GHC generated code is unsuitable for hard-real-time/embedded environments (although I would argue that it’s actually fine for general purpose OS programming). However, as far as hardware goes, the semantics of (a non-monomorphically-recursive subset of) Haskell is actually a surprisingly close match for the semantics of hardware (as in LUTs and flip-flops, not as in random microcontrollers). This is the basis of projects like Clash (Haskell to HDLs). I imagine one could extend the clash approach to generate allocation-free assembly from the same (large) subset of Haskell.

I don't have much experience with OCaml but my experience with ATS is that it's very much possible to have functional, ML-style programming without a runtime or even dynamic memory allocation.

...

It’s possible to write low-allocation (I wouldn’t call it “allocation free” - usually just the hot loops don’t allocate) OCaml with the standard tools. However, it requires a fairly non-idiomatic style. —Will

tower? atom?

Kind of tangential, but bluespev verilog is a "Haskell inspired" version of verilog that has a strong Haskell flavour (typeclasses, purity, a rudimentary effect system that tracks combinational versus state based logic, clock domains embedded into the type, width polymorphic functions, etc). It's a really great way to see what a haskell-like-hardware description language could look like :) Cheers siddharth On Sun 21 Oct, 2018, 12:34 Joachim Durchholz, wrote:

Am 21.10.18 um 04:52 schrieb Will Yager:

...

This is the basis of projects like Clash (Haskell to HDLs). I imagine

one could extend the clash approach to generate allocation-free assembly from the same (large) subset of Haskell.

Is that subset described somewhere?

Regards, Jo _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- Sending this from my phone, please excuse any typos!

Am 21.10.18 um 19:43 schrieb Vanessa McHale:

I've never understood why functional (and in particular Haskell-influenced) approaches to hardware never took off. I suspect it was political (Haskell is too academic, etc.), or perhaps the companies using it are just quiet about it :)

The usual reason is that they simply haven't seen it work, and are not sure whether it will work. Also, retraining your engineers is VERY expensive: expect a few weeks of training, plus a few months of reduced effectivity; multiply with an engineer's cost per month, and you arrive at really impressive figures. If a company is successful, it sees no reason to go into that risk. If a company is at the brink of defaulting, it cannot afford to try. It's usually the second-in-line companies that try this kind of stuff, and only if they have some risk appetite and need/want to catch up. In these companies, there's room for experiment - but the experiment needs to show success to be adopted, which is by no means guaranteed (you can easily fail with a better methodology if you don't do it right). And maybe functional really isn't a good match for hardware. I don't expect that to be reality, but I have too little experience with functional and almost zero with hardware, so I may be overlooking stuff - the design space for hardware is pretty different than the design space for software, pretty restrictive in some ways and unexpectedly flexible in others. Which brings me to another possible reason: Maybe functional isn't solving any of the real problems in hardware design. That would then be the "meh, nice but useless" reaction. Just speculating about possibilities here; as I said: too little hardware design experience here. Regards, Jo

On Sun, Oct 21, 2018 at 3:04 PM Joachim Durchholz wrote:

Is that subset described somewhere?

So there are two possible answers to this: 1. The subset that Clash supports is a bit complicated and increases from time to time, depending mostly on the internal details of the clash compiler 2. The subset that Clash *could* support with (roughly) its current approach, which I think I can answer a bit better: I gave a brief hand-wavy description earlier - "non-monomorphically-recursive" That is, any recursion has to be unrolled at the hardware level, and monomorphically (i.e. normally) recursive functions cannot (generally) stop being unrolled after a finite number of iterations. Sure, you can sometimes use fancy tricks (an SMT solver or something) to prove termination, but these come with a number of other challenges. For hardware you want a small, concrete number of recursions, which leads to lots of complications (e.g. need for dependent types to relate input values and recursion depth). Much simpler is to simply disallow monomorphic recursion, and then you shift the work of proving finite recursion depth to the type level. There's then a simple (constructive) rule for proving termination and calculating the number of recursive calls. Given F :: * -> * f :: a = ... (f :: F a) ... used at some site ... f ... 0. let seen_types = ∅ 1. let t = the type of "f" 2. If t ∈ seen_types, fail - unbounded recursion 3. Add t to seen_types 4. Inline the definition of "f" 5. Goto 1, with any newly introduced call to "f" This construction inlines every recursive call, which gives you a hardware-friendly representation without recursion at the end. This also supports multiple recursion, like over a binary tree (important for efficient hardware). To give a concrete example of how this works, consider sum :: ∀ n . Vec n Int -> Int sum :: Vec 0 Int -> Int = \Empty -> 0 -- Non-recursive sum :: Vec (n+1) Int -> Int = \(hd:tl) -> hd + (sum :: Vec n Int -> Int) tl This function is polymorphically recursive and perfectly reasonable to instantiate in hardware. The rule above succeeds in synthesizing the "sum" function, but will reject monomorphically recursive functions like "sum :: [Int] -> Int" or functions that end up being monomorphically recursive through a few polymorphically recursive "layers". One downside of this approach is that if F is divergent (i.e. the type of "f" never cycles back on itself but it always changes), this will either hang the compiler or you have to have an upper bound on the allowed number of inlines. This is probably fine - if you're trying to represent a function with a huge recursion depth in hardware, your design sucks and will be slow anyway. Again, reiterating that Clash doesn't *actually* support the entire subset mentioned above. That is just what one *could* support with the same conceptual approach. Instead, Clash has a few hard-coded things that it knows how to recurse over, like fixed-length vectors. There are probably some errors in the above - I'm not an expert on the internals of the clash compiler and this is just a brain-dump of my vague thoughts on synthesis. --Will

Anything that's tail recursive could be converted to a while loop and then clocked, no? You could for instance compile fact :: Int -> Int fact 0 = 1 fact n = n * fact (n - 1) to hardware even if it would not be a good idea. On 10/21/18 4:16 AM, William Yager wrote:

On Sun, Oct 21, 2018 at 3:04 PM Joachim Durchholz mailto:jo@durchholz.org> wrote:

Is that subset described somewhere?

So there are two possible answers to this:

1. The subset that Clash supports is a bit complicated and increases from time to time, depending mostly on the internal details of the clash compiler

2. The subset that Clash *could* support with (roughly) its current approach, which I think I can answer a bit better: 

I gave a brief hand-wavy description earlier - "non-monomorphically-recursive"

That is, any recursion has to be unrolled at the hardware level, and monomorphically (i.e. normally) recursive functions cannot (generally) stop being unrolled after a finite number of iterations. Sure, you can sometimes use fancy tricks (an SMT solver or something) to prove termination, but these come with a number of other challenges. For hardware you want a small, concrete number of recursions, which leads to lots of complications (e.g. need for dependent types to relate input values and recursion depth).

Much simpler is to simply disallow monomorphic recursion, and then you shift the work of proving finite recursion depth to the type level. 

There's then a simple (constructive) rule for proving termination and calculating the number of recursive calls.

Given

F :: * -> * f :: a = ... (f :: F a) ...

used at some site

... f ...

0. let seen_types = ∅ 1. let t = the type of "f" 2. If t ∈ seen_types, fail - unbounded recursion 3. Add t to seen_types 4. Inline the definition of "f" 5. Goto 1, with any newly introduced call to "f"

This construction inlines every recursive call, which gives you a hardware-friendly representation without recursion at the end. This also supports multiple recursion, like over a binary tree (important for efficient hardware). 

To give a concrete example of how this works, consider

sum :: ∀ n . Vec n Int -> Int sum :: Vec 0       Int -> Int = \Empty -> 0 -- Non-recursive sum :: Vec (n+1) Int -> Int = \(hd:tl) -> hd + (sum :: Vec n Int -> Int) tl

This function is polymorphically recursive and perfectly reasonable to instantiate in hardware. The rule above succeeds in synthesizing the "sum" function, but will reject monomorphically recursive functions like "sum :: [Int] -> Int" or functions that end up being monomorphically recursive through a few polymorphically recursive "layers".

One downside of this approach is that if F is divergent (i.e. the type of "f" never cycles back on itself but it always changes), this will either hang the compiler or you have to have an upper bound on the allowed number of inlines. This is probably fine - if you're trying to represent a function with a huge recursion depth in hardware, your design sucks and will be slow anyway.

Again, reiterating that Clash doesn't *actually* support the entire subset mentioned above. That is just what one *could* support with the same conceptual approach. Instead, Clash has a few hard-coded things that it knows how to recurse over, like fixed-length vectors.

There are probably some errors in the above - I'm not an expert on the internals of the clash compiler and this is just a brain-dump of my vague thoughts on synthesis.

--Will 

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.