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

André Muricy introduces the Agda programming language, explaining dependent types, propositions as types, and how they ensure code correctness.

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 gist.github.com/amuricys/5710e9a45705765ec11d1e3879e9ed4e André Muricy FP developer at Ada Beat. linkedin.com/in/amuricys/ Venue sponsor - Kivra kivra.se Video sponsor – Ada Beat adabeat.com Merch If you want to spread functional programming and support the channel, buy something from the shop: 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