Lean multimedia interactive capabilities

Stream: lean4

[Ioannis Konstantoulas]

Suppose that I am on an Xorg system and I want to write a native linux program, purely in Lean, that does the following:

1) It draws a window of given dimensions that contains a white background, a stickman figure on the bottom left, and an elevated platform (horizontal line segment) somewhere near the middle bottom.

2) When I press the left/right arrow keys, the stickman figure moves accordingly; holding the keys makes the figure move smoothly across the screen.

3) When I press the up key, the figure jumps up and lands down according to simple physics. Combining the up and horizontal keys, it jumps diagonally, allowing it to land on the platform.

4) If the figure lands on the platform, the speakers make a high pitched sound. If it jumps back on the ground, the speakers make a thud.

5) The program terminates after 2 minutes.

If I am correct, Lean cannot do most of these things right now by itself (without interfacing to some C library). My question is: what kind of infrastructure does Lean need to build, say in Std, in order to be able to write a program like the above?

Note: I do not want to assume any library like GTK or Qt, rather I want to write all the low level primitives in Lean.

[Mario Carneiro]

I don't think you can directly write the necessary glue code in lean, it doesn't have enough expressivity to express all C ABIs you will need to deal with to do this. If you are willing to settle for "writing C code in a Lean file" the closest thing is Alloy

[Mario Carneiro]

If you are willing to grant such glue code for OS interaction, it's still a bit of a challenge to write a graphics library

[Mario Carneiro]

I imagine that something like Handmade Hero would be a good reference, although it's somewhat windows-centric

[Ioannis Konstantoulas]

I understand; I only care about a very primitive multimedia IO (without performance goals and stickman-level :laughing: ), mostly to play with a domain well outside Lean's core competency. I am mostly curious as to what the underlying IO structures will look like in Lean.

[Mario Carneiro]

The main challenge will be grokking the shape of the windows / osx / linux APIs for graphics / other multimedia, which I'm sure are huge and complex even if you just want a hello world example

[Mario Carneiro]

a tutorial sounds like the best place to start

[Mario Carneiro]

writing the glue code and API in lean will be comparatively simple, once you know what you are dealing with

[Patrick Massot]

Why would anyone do that? Is there any language that play that game?

[Mario Carneiro]

??? Is there a programming language that does graphics?

[Patrick Massot]

I mean beyond C of course.

[Patrick Massot]

Is there a high-level programming language that play that game instead of interfacing with C libraries?

[Mario Carneiro]

Some languages can write the interfacing code in the native langauge

[Mario Carneiro]

ultimately it always bottoms out on a C interface, although it's not necessarily C on the other side

[Mario Carneiro]

To quote from a very lovely article C isn't a programming language anymore:

My problem is that C was elevated to a role of prestige and power, its reign so absolute and eternal that it has completely distorted the way we speak to each other. Rust and Swift cannot simply speak their native and comfortable tongues – they must instead wrap themselves in a grotesque simulacra of C’s skin and make their flesh undulate in the same ways it does.

[Julian Berman]

Depending on what counts here, there things like https://github.com/python-xlib/python-xlib

[Julian Berman]

(Which yeah perhaps writing an Xlib client in Lean is some sort of target, though the above platform-specific comments of course apply there)

[Alex J. Best]

@Anders Christiansen Sørby was implementing SDL bindings for Lean at some point btw at https://github.com/Anderssorby/SDL.lean, not sure what the status of that is now though.