[Haskell-cafe] Well typed OS

[Yotam Ohad]

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

[Joachim Durchholz]

Post by Yotam Ohad
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.

An OS needs to work for any programming language, so I'm not sure how to
get from an IO-based approach to a working OS. Unless you plan to write
the OS itself in Haskell and make it so that all programs are Haskell
modules, but that's a huge task.

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.
See https://en.wikipedia.org/wiki/Capability-based_security . This
article also has a link to other security models; capabilities are
pretty famous, but it's quite possible that a different one would be a
better fit.

HTH
Jo

[Ivan Perez]

Post by Joachim Durchholz

Post by Yotam Ohad
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.

An OS needs to work for any programming language, so I'm not sure how to
get from an IO-based approach to a working OS. Unless you plan to write
the OS itself in Haskell and make it so that all programs are Haskell
modules, but that's a huge task.

He seems to suggest that he is playing around with the idea, more than
proposing to write a whole OS.

For the sake of the exercise, it makes sense to assume that all programs
will carry a type specification.

Post by Joachim Durchholz
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?

As an exercise, I think this could be nice. And my intuition would be to
use specific effects/monads as well, both to provide the capabilities
themselves and to encode the idea that that permission or effect is needed.
Type inference might be able to tell you whether a permission may be needed
at all or not, so this seems like a potentially good idea.

The idea of using a less-than-IO monad to limit possible IO effects is not
uncommon. We briefly used it in [1, Section 7.3 - Limiting the Impact of
IO] and I seem to recall Thorsten Altenkirsch talking about this (I don't
remember if there's a paper and could not find one right now).

There's two parts to this problem: can I write Haskell programs with
limited-IO type specifications, and I think the answer is yes, and can I
ensure that programs will not use resources not declared in their type, and
I think the answer depends on kernel and, possibly, hardware support (even
if you restrict this to Haskell).

Because the type is not included in the program, it would not be included
with the executable. It would be interesting to output that too in some
form during compilation. This would seem also useful for DSLs.

Best wishes,

Ivan

[1] https://dl.acm.org/citation.cfm?id=2976010

[Joachim Durchholz]

Post by Joachim Durchholz
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.

[Vanessa McHale]

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.

As for effect types - the IO monad in Haskell exists primarily to allow
side effects in a lazy language, so there's no reason I see to keep it
in an operating system.

Post by Joachim Durchholz

Post by Yotam Ohad
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.

An OS needs to work for any programming language, so I'm not sure how
to get from an IO-based approach to a working OS. Unless you plan to
write the OS itself in Haskell and make it so that all programs are
Haskell modules, but that's a huge task.
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.
See https://en.wikipedia.org/wiki/Capability-based_security . This
article also has a link to other security models; capabilities are
pretty famous, but it's quite possible that a different one would be a
better fit.
HTH
Jo
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[MarLinn]

Post by Vanessa McHale
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

[Brandon Allbery]

I was thinking typed LLVM.

Post by Vanessa McHale
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Joachim Durchholz]

Post by 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

[Vanessa McHale]

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.

Post by Vanessa McHale
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Ivan Perez]

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

Post by Vanessa McHale
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.

Post by Vanessa McHale
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
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[MarLinn]

Hi Yotam,

one rather small and abstract comment:

Permissions and capabilities feel like they are something contravariant.
Intuitively it should be easy to "get out" of permissions but hard to
"get into" them. (compare 'pure' and 'extract')

Resulting actions are probably covariant just like the more general IO.

Therefore I conclude that programs in your OS will probably be a
profunctor, an arrow, or something similar. I wouldn't even be surprised
if one could build an OS on nothing but Optics into the RealWorld.

Cheers,
MarLinn

[John Z.]

Post by Yotam Ohad
Hi,
...
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.

For this specific example, it might be enough to just use something like
Turtle from Gabriel Gonzales:

http://hackage.haskell.org/package/turtle

which -to me- signals that problem doesn't necessarily have to stretch
so far as to implement a whole OS. Maybe just fixing smaller pieces here
and there would provide much higher bang for the buck.

[Barak A. Pearlmutter]

At a high level, you seem to be proposing encoding and enforcing
safety properties of executables using a type system. One
instantiation of this idea is proof-carrying-code (Necula and Lee,
1996, see https://en.wikipedia.org/wiki/Proof-carrying_code), which
ensures safety properties of machine code. The spin-off Cedilla
Systems built a mobile OS (intended for phones) around this, with the
idea that third-party apps would run unprotected with safety
guaranteed solely by sophisticated use of types. The Fox Project,
http://www.cs.cmu.edu/~fox/, was philosophically similar, and their
web page contains a bunch of interesting pointers to relevant work.

For whatever reason, this stuff never got much penetration. But in
today's Internet of Things, with malware being injected into mobile
phones and cars and light bulbs and toothbrushes and smart dust, it
may deserve another look.

[Alexander Kjeldaas]

You could consider the compiler for the IO type part of the TCB and execute
source code with caching, like nix. Every process could be wrapped in an IO
sandbox that is enforcing the types for all IO operations.

That just requires being able to implement a->Maybe b i.e. have a fixed
binary representation for the data in and out of the inner program.

Something like rudimentary programmable scripts that run on kernel system
call invocations already exists in Linux, so it could be possible to
compile down to that.

Alexander

Post by Barak A. Pearlmutter
At a high level, you seem to be proposing encoding and enforcing
safety properties of executables using a type system. One
instantiation of this idea is proof-carrying-code (Necula and Lee,
1996, see https://en.wikipedia.org/wiki/Proof-carrying_code), which
ensures safety properties of machine code. The spin-off Cedilla
Systems built a mobile OS (intended for phones) around this, with the
idea that third-party apps would run unprotected with safety
guaranteed solely by sophisticated use of types. The Fox Project,
http://www.cs.cmu.edu/~fox/, was philosophically similar, and their
web page contains a bunch of interesting pointers to relevant work.
For whatever reason, this stuff never got much penetration. But in
today's Internet of Things, with malware being injected into mobile
phones and cars and light bulbs and toothbrushes and smart dust, it
may deserve another look.
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[William Yager]

Post by Barak A. Pearlmutter
At a high level, you seem to be proposing encoding and enforcing
safety properties of executables using a type system. One
instantiation of this idea is proof-carrying-code (Necula and Lee,
1996, see https://en.wikipedia.org/wiki/Proof-carrying_code), which
ensures safety properties of machine code.

I would guess a factor that prevented something like PCC from taking off is
the fact that proofs over binaries are relatively pretty challenging to
express and verify, and ISA semantics tend to be really complicated.

I think an intermediate approach that might be a lot cheaper to implement
is to ship some sort of IR (rather than machine code) that is A) relatively
cheap to check and compile and B) carries some variety of safety guarantee.

As I recall, A) is already in use. Apple requires developers to submit
applications as LLVM IR rather than machine code.

LLVM IR definitely isn't designed with B) in mind, however. I could imagine
something like Core being useful here. A fully annotated type-checked
language with semantics amenable to formal analysis.

You could add some sort of effects system to the type system of the IR, as
a basis for enforcing security policies. E.g. network access could be an
effect.

The advantage of doing this over PCC is that we don't have to retrofit the
proof system to match the ISA, but instead can design the IR specifically
to make the proof system easy. A downside is that you have to compile the
application once upon downloading it, but this doesn't seem to cause too
much of an issue in practice.

[Barak A. Pearlmutter]

I would guess a factor that prevented something like PCC from taking off is the fact that proofs over binaries are relatively pretty challenging to express and verify, and ISA semantics tend to be really complicated.

The Cedilla folks had a pretty clever way of dealing with that issue.
They had a very small proof checker on the embedded device, which used
highly compressed information associated with the binary to basically
guide a theorem prover, where the information helped the prover make
all its choices.

This information was generated from a proof generated by a compiler,
which compiled a high-level language (C in their case) annotated with
extra safety-proof-related information down to both machine code an a
proof of that machine code's safety. So they sort of did what you're
describing, but partially evaluated away the IR.

[Ionuț G. Stan]

The JVM is also doing something similar. There's a step in the process
of loading the .class files called "bytecode verification". Ιt's
basically a type checker for the stack language used in the bytecode.

This was problematic in Java before version 7, because it was possible
to cause denial-of-service attacks by sending malicious bytecode
payloads. The verifier would spend O(n^2) time verifying that the
bytecode behaves correctly.

As of Java 7, compilers are required to add additional info alongside
the bytecode instructions. This extra info is called a stackmap table
and allows the verifier to complete its verification in O(n) steps,
IIRC. So, a certain instantiation of PPC is already used in the wild.

Post by Barak A. Pearlmutter

I would guess a factor that prevented something like PCC from taking off is the fact that proofs over binaries are relatively pretty challenging to express and verify, and ISA semantics tend to be really complicated.

The Cedilla folks had a pretty clever way of dealing with that issue.
They had a very small proof checker on the embedded device, which used
highly compressed information associated with the binary to basically
guide a theorem prover, where the information helped the prover make
all its choices.
This information was generated from a proof generated by a compiler,
which compiled a high-level language (C in their case) annotated with
extra safety-proof-related information down to both machine code an a
proof of that machine code's safety. So they sort of did what you're
describing, but partially evaluated away the IR.
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Joachim Durchholz]

Post by Ionuț G. Stan
The JVM is also doing something similar. There's a step in the process
of loading the .class files called "bytecode verification". Ιt's
basically a type checker for the stack language used in the bytecode.

It's checking more than just types:

* Branch target and exception handler address validity.
* Stack offset validity.
* Each code branch ends with a return instruction.
* Local variables initialized before use in each branch of code.
* No stack overflow or underflow along each code path.
* Validation of private and protected access.

I suspect that all of this can be expressed as a type check, but some of
them require that a type be generated for each natural number that's in
the class file, and I have yet to see an approach that gives each of
these types a printable, humanly understandable representation.

[Ionuț G. Stan]

Post by Joachim Durchholz

Post by Ionuț G. Stan
The JVM is also doing something similar. There's a step in the process
of loading the .class files called "bytecode verification". Ιt's
basically a type checker for the stack language used in the bytecode.

Sure. I used an informal, hand-wavy sense for "type checker".

Post by Joachim Durchholz
* Branch target and exception handler address validity.
* Stack offset validity.
* Each code branch ends with a return instruction.
* Local variables initialized before use in each branch of code.
* No stack overflow or underflow along each code path.
* Validation of private and protected access.
I suspect that all of this can be expressed as a type check, but some of
them require that a type be generated for each natural number that's in
the class file, and I have yet to see an approach that gives each of
these types a printable, humanly understandable representation.

Can you give a bit more detail here? Or a pointer to someone who
elaborated on this? I got a bit lost on the natural number step, which
seems to be some sort of theoretical way to represent those types. On
the other hand you say they're in the class file.

BTW, I'm quite familiar with the class file format and have even started
writing a bytecode verifier for my own compiler pet project. So, be as
specific as you can.

Post by Joachim Durchholz
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Joachim Durchholz]

Post by Ionuț G. Stan

Post by Joachim Durchholz
a type be generated for each natural number that's in
the class file, and I have yet to see an approach that gives each of
these types a printable, humanly understandable representation.

Can you give a bit more detail here? Or a pointer to someone who
elaborated on this? I got a bit lost on the natural number step, which
seems to be some sort of theoretical way to represent those types.

You can make Haskell's type system count, by defining a `Zero` type and
a `Succ a` type - well, I think it's a kind (i.e. a type of types). That
(and equality) is enough to do natural numbers - you have Zero, One =
Succ Zero, Two = Succ Succ Zero, etc.

I don't know enough about this stuff to give a recipe, I just saw
descriptons of what people were doing.
The earliest awesome trick of this kind was somebody who encoded matrix
squareness in the type system. (You cannot even define inversion for a
non-square matrix, so square matrices are pretty different beasts than
non-square ones.)
Somebody else (I think) started doing the natural numbers. You can do
any kinds of cool tricks with that, such as cleanly expressing that to
multiply two matrices, the height of one matrix needs to be the same as
the width of the other.

In theory, you can express any arithmetic relationships within the type
system that way: Addresses, matrix dimension constraints, etc.
In practice, any error messages are going to look like "invalid type
Succ Succ Succ .... Succ Zero", and you have to count the number of
Succs, which sucks (pun intended).

I suspect you can also do fractional numbers with that - you essentially
translate the axioms some type (or kind) declarations.
I'd expect that to be even less usable in practice.
However, it's intriguing what you can do with types.

Now please take this all with a grain of salt. I never used this kind of
stuff in practice, I just saw the reports of people doing this clever
insanity, and didn't want to do it myself.
The approach never took on if this kind of old lore isn't present in
Haskell Café anymore.

Post by Ionuț G. Stan
BTW, I'm quite familiar with the class file format and have even started
writing a bytecode verifier for my own compiler pet project. So, be as
specific as you can.

I was more like handwaving at the possibility of turning all assertions
over integral numbers into type constraints.
I am definitely not recommending doing this in practice!

Regards,
Jo

[Vanessa McHale]

The problem with an IR is that some languages would inevitably suffer -
LLVM in particular was designed as a backend for a C compiler, and so it
is not necessarily well-suited for lazy languages, immutable languages,
etc. (not to mention self-modifying assembly and other such pathological
beasts...)

On Sat, Oct 6, 2018 at 11:03 PM Barak A. Pearlmutter
At a high level, you seem to be proposing encoding and enforcing
safety properties of executables using a type system. One
instantiation of this idea is proof-carrying-code (Necula and Lee,
1996, see https://en.wikipedia.org/wiki/Proof-carrying_code), which
ensures safety properties of machine code. 
I would guess a factor that prevented something like PCC from taking
off is the fact that proofs over binaries are relatively pretty
challenging to express and verify, and ISA semantics tend to be really
complicated.
I think an intermediate approach that might be a lot cheaper to
implement is to ship some sort of IR (rather than machine code) that
is A) relatively cheap to check and compile and B) carries some
variety of safety guarantee.
As I recall, A) is already in use. Apple requires developers to submit
applications as LLVM IR rather than machine code.
LLVM IR definitely isn't designed with B) in mind, however. I could
imagine something like Core being useful here. A fully annotated
type-checked language with semantics amenable to formal analysis.
You could add some sort of effects system to the type system of the
IR, as a basis for enforcing security policies. E.g. network access
could be an effect.
The advantage of doing this over PCC is that we don't have to retrofit
the proof system to match the ISA, but instead can design the IR
specifically to make the proof system easy. A downside is that you
have to compile the application once upon downloading it, but this
doesn't seem to cause too much of an issue in practice.
  
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Joachim Durchholz]

Post by Vanessa McHale
The problem with an IR is that some languages would inevitably suffer -
LLVM in particular was designed as a backend for a C compiler, and so it
is not necessarily well-suited for lazy languages, immutable languages,
etc. (not to mention self-modifying assembly and other such pathological
beasts...)

Actually LLVM is built for being adaptable to different kinds of
languages. It does have a bias towards C-style languages, but you can
adapt what doesn't fit your needs *and still keep the rest*.

The following was true a few years ago:

When I asked, the LLVM IR was intentionally not specified to be reusable
across languages, so that different compiler toolchain could adapt the
IR to whatever needs their language or backend infrastructure needed.

Garbage collection is one area where you have to do a lot of work. There
are some primitive instructions that support it, but the semantics is
vague and doesn't cover all kinds of write barriers. You'll have to roll
your own IR extensions - or maybe I didn't understand the primitives
well enough to see how much they cover.
Anyway, LLVM does not come with a GC implementation.
OTOH, it does not prevent you from doing a GC. In particular, you're
free to avoid C-style pointers, so you have the full range of GC
algorithms available.

Laziness? No problem. If you do tagless/spineless, you'll code the
evaluation machine anyway. Just add an IR instructions that calls the
interpreter.

Immutability? No problem - actually nowhere a problem. Immutability
happens at the language level, at the IR level it is pretty irrelevant
because compilers try to replace object copying by in-place modification
wherever possible, anyway.

Self-modifying assembly? No IR really supports that. Mostly it's
backends that generate self-modifying code from IR instructions for
specific backends.

TL;DR: For its generality, LLVM IR is better suited to languages with
specific needs in the backend than anything else that I have seen (which
means C runtimes, various VM proofs of concept which don't really count,
and JVM - in particular I don't know how .net compares).

Regards,
Jo

[Gleb Popov]

Post by Joachim Durchholz

Post by Vanessa McHale
The problem with an IR is that some languages would inevitably suffer -
LLVM in particular was designed as a backend for a C compiler, and so it
is not necessarily well-suited for lazy languages, immutable languages,
etc. (not to mention self-modifying assembly and other such pathological
beasts...)

Actually LLVM is built for being adaptable to different kinds of
languages. It does have a bias towards C-style languages, but you can
adapt what doesn't fit your needs *and still keep the rest*.
When I asked, the LLVM IR was intentionally not specified to be reusable
across languages, so that different compiler toolchain could adapt the
IR to whatever needs their language or backend infrastructure needed.
Garbage collection is one area where you have to do a lot of work. There
are some primitive instructions that support it, but the semantics is
vague and doesn't cover all kinds of write barriers. You'll have to roll
your own IR extensions - or maybe I didn't understand the primitives
well enough to see how much they cover.
Anyway, LLVM does not come with a GC implementation.
OTOH, it does not prevent you from doing a GC. In particular, you're
free to avoid C-style pointers, so you have the full range of GC
algorithms available.
Laziness? No problem. If you do tagless/spineless, you'll code the
evaluation machine anyway. Just add an IR instructions that calls the
interpreter.

I'm far from expert in this area, but isn't that "interpreter" a simple yet
slow approach to codegen? My understanding is that when you use, say, a
global variable as a register for your evaluation machine, it is slower
than if you somehow pin real hardware register for that purpose. I think
this is what "registerized" GHC build means.
In LLVM you can't use, say, RSP in a way you want, but it is doomed to be
"stack pointer register", even if you don't use stack at all.

As I read in some blog, you can slightly affect LLVM codegen by adding
calling conventions, but the real solution would be another algorithm for
instruction selection. No one implemented that yet, AFAIK.

Post by Joachim Durchholz
Immutability? No problem - actually nowhere a problem. Immutability
happens at the language level, at the IR level it is pretty irrelevant
because compilers try to replace object copying by in-place modification
wherever possible, anyway.
Self-modifying assembly? No IR really supports that. Mostly it's
backends that generate self-modifying code from IR instructions for
specific backends.
TL;DR: For its generality, LLVM IR is better suited to languages with
specific needs in the backend than anything else that I have seen (which
means C runtimes, various VM proofs of concept which don't really count,
and JVM - in particular I don't know how .net compares).
Regards,
Jo
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Joachim Durchholz]

Post by Joachim Durchholz
Laziness? No problem. If you do tagless/spineless, you'll code the
evaluation machine anyway. Just add an IR instructions that calls the
interpreter.
I'm far from expert in this area, but isn't that "interpreter" a simple
yet slow approach to codegen? My understanding is that when you use,
say, a global variable as a register for your evaluation machine, it is
slower than if you somehow pin real hardware register for that purpose.
I think this is what "registerized" GHC build means.

My impression has been that GHC is compiling everything down to machine
code. FWIW most mentions I saw were of the kind "we replace
tagless/spineless with X", not of the "we build on tagless/spineless
doing Y". Not that I have read many papers - I'm awfully behind on these
topics.

Post by Joachim Durchholz
In LLVM you can't use, say, RSP in a way you want, but it is doomed to
be "stack pointer register", even if you don't use stack at all.

Actually it seems possible since some version between 3.4 and 3.6.
https://stackoverflow.com/questions/29365198/how-to-use-llvm-intrinsics-llvm-read-register
discusses a way of doing exactly that.

Not sure about ramifications though.

Still, seeing how many wildly varying languages use LLVM for code
generation, it seems to be widely considered to be the most flexible
available one.
If somebody knows of something more flexible, paint me interested :-)

Regards,
Jo

[Andreas Reuleaux]

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

Post by Yotam Ohad
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Vanessa McHale]

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.

Post by Andreas Reuleaux
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

Post by Yotam Ohad
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
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Jeffrey Brown]

I don't know whether this is helpful, but Purescript provides a way to
specify the kinds of IO a monad can do. For instance, the Extensible

:type main

forall eff. Eff (console :: CONSOLE, random :: RANDOM | eff) Unit

[1] https://leanpub.com/purescript/read#leanpub-auto-extensible-effects

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.

Post by Andreas Reuleaux
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

Post by Yotam Ohad
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

Post by Andreas Reuleaux

Post by Yotam Ohad
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

Post by Andreas Reuleaux

Post by Yotam Ohad
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
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
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Will Yager]

Post by Vanessa McHale
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.

Post by Vanessa McHale
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

[Vanessa McHale]

Interesting! It's been awhile since I've worked on FPGAs :)

ATS is the only language I've seen that advertises stack-allocated
closures, and I think GHC's approach to laziness requires heap
allocation, so there's still a few targets (AVR off the top of my head)
that GHC would need significant modification to work on.

Post by Vanessa McHale
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.

Post by Vanessa McHale
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

[Raoul Duke]

tower? atom?

[Joachim Durchholz]

Post by 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

[Siddharth Bhat]

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

Post by Will Yager

Post by 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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[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 :)

I think you could use monads for clock domains. Once something has a
clocked input, its output will be clocked too - it fits well with the
"lift anything unclocked to clocked, but once clocked it is *always*
clocked".

Post by Siddharth Bhat
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

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
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!
_______________________________________________
Haskell-Cafe mailing list
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Joachim Durchholz]

Post by 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

[Will Yager]

or perhaps the companies using it are just quiet about it :)

It’s this. There are some companies you’ve heard of who are using it quietly :)

Anything that's tail recursive could be converted to a while loop and then clocked, no?

Yes, but the semantics of this are very different and the translation is much less straightforward (eg how many iterations will it take?). Better to do this “manually”, imo. Construct a mealy machine or something.

[William Yager]

Post by Joachim Durchholz
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

[Joachim Durchholz]

Post by William Yager
2. The subset that Clash *could* support with (roughly) its current

Thanks - that's exactly what I was after.

[Vanessa McHale]

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.

Post by Joachim Durchholz
Is that subset described somewhere?
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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

[Vanessa McHale]

Others know more than I but the gist of it is that you can compile
functions to circuits. Haskell's functions are fundamentally different
from C's functions (which are basically procedures that sometimes have a
return value), but there's no reason you can't compile a non-strict
function to a circuit.

Post by Joachim Durchholz

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
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.