Put A Type On It: Idris Type Providers for AWS Resources
summary
Claims an Idris type provider that reads AWS VPC and subnet metadata to compute account/region specifics (example: US West 1 two AZs, US West 2 three, US East 1 four) and generates types that encode deployment rules. It builds functions to enforce security, availability and cost policies, can validate existing deployments and produce pre-deploy plans, targets total checking for stronger guarantees, and is available as a GitHub prototype that the uploader promises to publish.
AI-written summary · about
chapters (24)
- 0:00Introduction
- 0:32Who am I
- 1:49Questions
- 2:08Type Errors
- 3:48Availability Zones
- 4:59The Problem
- 6:03The Solution
- 8:21Why Infrastructure
- 10:06What is a Type Provider
- 11:26How Type Providers Work
- 12:37Idris Type Providers
- 15:27CSV Type Provider
- 16:39Using Idris Type Provider
- 22:01Review
- 24:53Negation
- 25:25Conjunction
- 25:58Disjunction
- 26:33Consistency
- 27:09Total
- 27:36Induction
- 29:40Qualifier
- 30:10Existential Quantifier
- 30:32Proof
- 31:29Encoding Infrastructure
related talks
05mIdris (Lightning Talk)
39mYou Got Your Idris in My C++! A First Look at Denotational Design
30mWhy I Needed Rust: Finally, Infrastructure Automation I can sleep on
35mBuilding composable web services with Axum
24mArchitecting Ambient Mesh for Scale
32mTour of language landscape
36mFunctional State Machines in Rust: Typestate and Newtype Patterns
01h 01mPractical Type Erasure