In my post my post about where I intend to go with this blog for the next little while, I mentioned that I wanted to work with the Scheme programming language. However, I gave it some more thought and I decided against it for two reasons. The first reason is that the scheme specification drama is just a mess. I have no interest in deep diving into a flame war and coming out with a language I'd most likely be partially unsatisfied with. The second reason is that since I have ambitions towards working with and creating dependently typed programming languages, I thought I'd give Lean, the hot new dependently typed language on the block, a test drive.
The Lean programming language is pretty much exclusively known for mathlib, its most popular library that contains proofs for more math than most people ever learn due to a lot of attention given by the broader math community. However, Lean was developed with general purpose programming in mind. There appears to be efforts being made towards creating a standard library and there's also a guide on how to do functional programming with this language. I just started fumbling around with this guide and so I thought I'd share my first hello world program in lean.
I'll be sharing code in the following form and refer to these forms as "files" that live in a "repository":
|
<The Repository Name>;
<The File Name>; |
|---|
|
<First line of code>
<Second line of code>
|
|
<Output from the code>
|
A hello world program in Lean is very simple to write. Since that's the case, I'll also showcase some file structure, string interpolation, and comments in lean.
|
HelloWorld;
HelloWorld/Basic.lean; |
|---|
|
/-
We define the variable hello with type String
to have the value "world".
-/
def hello : String := "world"
|
|
HelloWorld;
HelloWorld.lean; |
|---|
|
import HelloWorld.Basic
|
|
HelloWorld;
Main.lean; |
|---|
|
import HelloWorld
def main : IO Unit := IO.println s!"Hello, {hello}!"
|
|
Hello, World!
|
I'm aware that this syntax is closely related to how haskell does things but I'm not yet prepared to go into detail about how this works exactly. I hope to do so in the future!