this post was submitted on 25 Feb 2025
6 points (100.0% liked)

The Firehose

1 readers
28 users here now

MY PERSONAL COMMUNITY.

I tend to overshare all of the things I am into, creating a wall of links that people can't keep up with.

Therefore, I decided to aggregate all of the links in one place for others to see.

I am the only person that can post here because this is my personal collection of links.

Rules (anyone that violates them will be promptly banned for life):

  1. These is my community to aggregate my favorite links. I am not a "bot". If you don't like it, please make a comment and I will happily ban you for life.

  2. Don't be a troll. This is completely up to my interpretation and I reserve the right to be a power tripping mod if I wish.

  3. If you're going to have a discussion, keep it civil. Don't gaslight people, gatekeep, move goalposts, etc.

  4. I am a leftist. Spamming this comm with viewpoints that I deem right wing or fascist will get you banned.

  5. No neoliberal genocide apologia and identity politics bullshit. I will enthusiastically ban you with prejudice.

founded 1 day ago
MODERATORS
[email protected]
6
"Super Haskell": an introduction to Agda by André Muricy (youtu.be)
submitted 1 day ago by [email protected] to c/[email protected]
0 comments fedilink hide all child comments
 

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)

no comments (yet)
sorted by: hot top controversial new old
there doesn't seem to be anything here