Skip to content
Hallway
0:00 / 0:00

#idris#dependenttypes#monoids

Idris: verifying a monoid

Brian McKenna

1.4K subscribers • 4 videos on Hallway

YouTube
  • Recommended by 2 people: 1 on Lobsters and 1 in engineering communities.
  • Presented by Brian McKenna

Intermediate. Assumes working knowledge.

6.3K views12 years ago2 recommendations

Programming languagesComputer scienceFunctional programmingFormal methods and verification

Brian McKenna demonstrates how to use Idris to verify that a monoid instance satisfies the associativity, left identity, and right identity laws.

Ensuring an instance of the Monoid type-class actually satisfies the "monoid laws" (i.e. associativity, left identity and right identity) using Idris, a dependently typed programming language. The result is here: gist.github.com/puffnfresh/11360808

Why it's here

2 people recommend this

u/dotneterin r/haskell • Recommends

Verifying the monoid laws using Idris
39View on Reddit

bitemyappon Lobsters • Recommends

Idris: verifying a monoid - YouTube
10View on Lobsters

bitemyappon Lobsters • Recommends

Verifying a monoid
6View on Lobsters

u/Titanlegionsin r/haskell • Mentions

On “Creating a "Group" Type Class”

Have a look at this for an example of how to so this sort of thing in Idris.
3View on Reddit