I'm one of the developers working on Formality and want to add a some links to:<p>- Our docs (docs.formality-lang.org)<p>- Our standard library (<a href="https://github.com/moonad/Formality-Base" rel="nofollow">https://github.com/moonad/Formality-Base</a>)<p>- Our Telegram channel (<a href="https://t.me/formality_lang" rel="nofollow">https://t.me/formality_lang</a>)<p>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.<p>Haskell can do this too, of course (as described in Gabriel Gonzalez's classic "Scrap your type classes" post <a href="http://www.haskellforall.com/2012/05/scrap-your-type-classes.html" rel="nofollow">http://www.haskellforall.com/2012/05/scrap-your-type-classes...</a>), 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.<p>For example, here's our Semigroup type:<p><pre><code> T Semigroup {A : Type}
| Semigroup
{ f : A -> A -> A
, associative : Associative(A,f)
}
</code></pre>
Where `Associative` is an abstract property defined in `Algebra.Magma` (<a href="https://github.com/moonad/Formality-Base/blob/master/Algebra.Magma.fm" rel="nofollow">https://github.com/moonad/Formality-Base/blob/master/Algebra...</a>)<p><pre><code> Associative : {A : Type, f : A -> A -> A} -> Type
{x : A, y : A, z : A} -> f(f(x,y),z) == f(x,f(y,z))
</code></pre>
Then if you want to instantiate a particular `Semigroup` you have to do:<p><pre><code> 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)
</code></pre>
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](<a href="https://argumatronic.com/posts/2019-06-21-algebra-cheatsheet.html" rel="nofollow">https://argumatronic.com/posts/2019-06-21-algebra-cheatsheet...</a>) has been an amazing resource.<p>Particular files in base that exemplify this are:<p>- Category.fm (<a href="https://github.com/moonad/Formality-Base/blob/master/Category.fm" rel="nofollow">https://github.com/moonad/Formality-Base/blob/master/Categor...</a>)<p>- Algebra.Lattice.fm (<a href="https://github.com/moonad/Formality-Base/blob/master/Algebra.Lattice.fm" rel="nofollow">https://github.com/moonad/Formality-Base/blob/master/Algebra...</a>)<p>- Control.Monad.fm (<a href="https://github.com/moonad/Formality-Base/blob/master/Control.Monad.fm" rel="nofollow">https://github.com/moonad/Formality-Base/blob/master/Control...</a>)<p>- Data.Maybe.Control (<a href="https://github.com/moonad/Formality-Base/blob/master/Data.Maybe.Control.fm" rel="nofollow">https://github.com/moonad/Formality-Base/blob/master/Data.Ma...</a>)<p>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 (<a href="https://t.me/formality_lang" rel="nofollow">https://t.me/formality_lang</a>) or even DM me directly! (I'm @johnburnham on TG)<p>Comment adapted from a post on the Haskell subreddit: <a href="https://www.reddit.com/r/haskell/comments/d2gcyw/just_letting_you_know_that_formality_has_evolved/" rel="nofollow">https://www.reddit.com/r/haskell/comments/d2gcyw/just_lettin...</a>