"Super Haskell": an introduction to Agda by André Muricy

André Muricy presents Agda, a dependently typed programming language, and its philosophy, motivation, and underlying theory. Agda aims to increase confidence in the correctness of code by allowing the expression of specific shapes or types for functions, reducing cognitive workload.

André introduces the concept of dependent types, which bridge the gap between human intention and machine code. He also discusses the importance of striking a balance between convenience and correctness in programming and the use of Agda mode for facilitating Agda programming in Integrated Development Environments (IDEs).

The video covers Agda's syntax, propositions as types, and functions, including the concept of propositions as types, uninhabited and inhabited types, bottom and top, and dependent functions. Muricy also discusses type-safe subtraction, vectors, the sigma type, and dependent products. The presentation concludes with a discussion on constructing and deconstructing matrices using Haskell and Agda, and the use of pragmas and postulates to interface with Haskell code and create functions.

Outline:
Syntax (defining types, functions etc)
Simple proofs
Simple programming
Dependently typed programming (sigma and pi types)

Code and more from the presentation
https://gist.github.com/amuricys/5710...

André Muricy
FP developer at Ada Beat.
  / amuricys  

Venue sponsor - Kivra
https://kivra.se

Video sponsor – Ada Beat
https://adabeat.com

Merch
If you want to spread functional programming and support the channel, buy something from the shop:
https://funcprogsweden.myspreadshop.net/

The chapters:
00:00 Welcome by Magnus Sedlacek
01:11 Thanks Kivra for the Venue
01:25 Thanks Ada Beat for the Video stream
02:49 “Super Haskell”: an introduction to Agda by André Muricy
03:35 Introduction of André Muricy and the presentation
04:41 Why dependently type?
06:12 The tools at our disposal
07:39 When it comes to types
08:16 Pluming in typed languages
09:12 Pluming in untyped languages
09:30 Pluming in super typed languages
10:33 Not having the right material
12:22 So what is Agda?
13:48 Time for code in Agda
14:41 Introduction of the syntax in Agda
17:13 Sum types and values
18:12 Either types and values
19:23 Product types and values
20:27 Tuple types and values
21:02 Functions, pattern matching
21:38 More syntactic things: let and where blocks
24:20 Propositions As Types
25:08 Equality type
29:25 Bottom and Top types (alarm goes off)
33:44 Strict inequality
37:40 Prototypical example
38:54 Take
39:55 Concatenation
40:30 Lookup
40:56 Singelton
41:45 Map
42:06 Pwise
42:31 replicate
43:10 transpose
44:05 zipWith
44:39 sigma type
48:03 Matrix
54:18 Pseudo Inverse
1:02:53 Conclusion
1:04:14 Q & A

#funcprogsweden