Formality, a (proof)gramming language featuring optimal reductions | Hacker News Reader

Formality, a (proof)gramming language featuring optimal reductions

github.com

27 pointsLightMachine8 comments

I haven’t been able to grok this formal logic stuff, so I just want to give props to the animation at the bottom of your git readme. It looks very... mathy yet playful and makes me want to know what’s happening :)

Surely the title should say "pro(of)gramming language", not "(proof)gramming language". What is a gramming language?

You have a point

I'm one of the developers working on Formality and want to add a some links to:

- Our docs (docs.formality-lang.org)

- Our standard library (https://github.com/moonad/Formality-Base)

- Our Telegram channel (https://t.me/formality_lang)

One thing I've been particularly enjoying with Formality is how we can implement structures like `Monoid`, `Profunctor`, `Monad`, etc. directly as types, rather than requiring type class machinery.

Haskell can do this too, of course (as described in Gabriel Gonzalez's classic "Scrap your type classes" post http://www.haskellforall.com/2012/05/scrap-your-type-classes...), but what's really neat about Formality is that we can package propositions inside our "class types", so that only lawful instances can be created.

For example, here's our Semigroup type:

    T Semigroup {A : Type}
    | Semigroup
      { f           : A -> A -> A
      , associative : Associative(A,f)
      }

Where `Associative` is an abstract property defined in `Algebra.Magma` (https://github.com/moonad/Formality-Base/blob/master/Algebra...)

    Associative : {A : Type, f : A -> A -> A} -> Type
       {x : A, y : A, z : A} -> f(f(x,y),z) == f(x,f(y,z))

Then if you want to instantiate a particular `Semigroup` you have to do:

    and.Semigroup : Semigroup(Bool)
      semigroup(~Bool, and, and.associative)

    and.associative : 
      { case a : Bool
      , case b : Bool
      , case c : Bool
      } -> and(and(a,b),c) == and(a,and(b,c))
    | true  true  true   => refl(~true)
    | true  true  false  => refl(~false)
    | true  false true   => refl(~false)
    | true  false false  => refl(~false)
    | false true  true   => refl(~false)
    | false true  false  => refl(~false)
    | false false true   => refl(~false)
    | false false false  => refl(~false)

Providing proofs all over the place is a lot of work, but it's been a really fun experience that's taught me a lot about different algebraic or category theoretic structures. Julie Moronuki's post on [algebraic structures](https://argumatronic.com/posts/2019-06-21-algebra-cheatsheet...) has been an amazing resource.

Particular files in base that exemplify this are:

- Category.fm (https://github.com/moonad/Formality-Base/blob/master/Categor...)

- Algebra.Lattice.fm (https://github.com/moonad/Formality-Base/blob/master/Algebra...)

- Control.Monad.fm (https://github.com/moonad/Formality-Base/blob/master/Control...)

- Data.Maybe.Control (https://github.com/moonad/Formality-Base/blob/master/Data.Ma...)

Still a ton of work to do, and a lot of these structures need instance proofs, so if anyone feels inspired, please don't hesitate to join our Telegram channel (https://t.me/formality_lang) or even DM me directly! (I'm @johnburnham on TG)

Comment adapted from a post on the Haskell subreddit: https://www.reddit.com/r/haskell/comments/d2gcyw/just_lettin...

Since this is Hacker News and not the Haskell subreddit, though, I feel obligated to answer the inevitable "Why should 'normal' developers care?" question that often comes up here whenever people talk about functional programming.

My answer is that I believe mathematics is worth doing, and that math has improved the human experience immeasurably, in aesthetics, in ethics, and, yes, also in commerce and technology. Given this, I want to build the best tools possible for enabling our collective exploration of math.

There's a wonderful result from programming language theory called the Curry-Howard isomorphism that says there is a correspondence between all of math and all of programming. Every program is a proof, every theorem is a type https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon.... This means we can (and should) use computers as mathematical prostheses, to enable each of our human brain's ability to reason in this field.

And, via Curry-Howard, if we can make it easier to reason about math using computers, we coincidentally will make it easier to reason about computers using math. The two fields are, in essence, the same.

TL;DR "You may not be interested in mathematics, but mathematics is interested in you!"

If I am not mistaken Agda is similar in this regard too. My question would be how is no garbage collection possible, or how practical is it to use an FP language without GC? I assume I can't get very far with writing ML-like programs without GC.

edit: nvm, just saw that it uses linear (or affine?) types

We use affine types, which means every value can get used at most once. This is a lot less painful in practice than it sounds though, since:

a. we can copy things for free at compile-time that get erased at runtime

b. we have a `cpy` primitive that allows for free copying of our Word type (a 32-bit unsigned int)

c. we have a primitive that allows for deep-copying, as long as the copies (and anything that uses them) are marked with usage annotations https://docs.formality-lang.org/en/latest/language/4.Core-Fe...

If you want faster adoption, have a repo that demonstrates solutions for 57 exercises: https://pragprog.com/book/bhwb/exercises-for-programmers

Reply on news.ycombinator.com