u/dmalikovin r/haskell • Recommends
Edwin Brady on Blodwen - Idris successor with Linear Types and Quantitative Type Theory
0:00 / 0:00
#idris#dependenttypes#type-drivendevelopment
Edwin Brady - Idris 2: Type-driven development of Idris | Code Mesh LDN 18
Code Sync
15K subscribers • 57 videos on Hallway
- Recommended by 8 people: 5 on Hacker News, 1 on Lobsters and 2 in engineering communities.
- Presented by Edwin Brady, creator of Idris
Intermediate. Assumes working knowledge.
19K views7 years ago8 recommendations
Programming languagesComputer scienceFunctional programmingComputation and complexityLanguage design and type systems
Edwin Brady introduces Idris 2, demonstrating how its dependently typed system can automatically implement functions from their type signatures.
This video was recorded at Code Mesh LDN 18 bit.ly/2P7SPII Get involved in Code Sync's next conference bit.ly/2Mcm4aS --- IDRIS 2: TYPE-DRIVEN DEVELOPMENT OF IDRIS by Edwin Brady THIS TALK IN THREE WORDS: Enthusiasm About Types :) TALK LEVEL: ABSTRACT We've been having lots of fun over the last couple of years investigating the possibilities and limitations of type-driven development in Idris. As we write larger programs, though, we're finding the implementation of Idris is showing the strain - such is the nature of "research quality software" - and recently I decided the time was right to start again, and implement Idris 2 in Idris. In this talk, I'll give an introduction to type-driven development (in Idris 2) and report on progress so far, showing off the most interesting features which the new design enables (notably, linear types and better type inference). Read the full abstract: codesync.global/speaker/edwin-brady/ --- THE SPEAKER - EDWIN BRADY Creator of the Idris programming language; Lecturer Edwin is Lecturer in Computer Science at the University of St Andrews in Scotland, interested in type-driven development, domain-specific languages and reasoning about effectful programs. When he's not doing that, he might be playing Go, watching cricket, or wandering around Scotland's hills. More on Edwin Brady: codesync.global/speaker/edwin-brady/ --- CODE SYNC & CODE MESH LDN 18 Code Mesh LDN is powered by Code Sync. Code Mesh LDN 18 was sponsored by WhatsApp, Toyota Connected, Erlang Solutions, TEAMango, and aeternity. CODE SYNC Website: www.codesync.global Twitter: www.twitter.com/CodeMeshIO Facebook: facebook.com/CodeSyncGlobal LinkedIn: linkedin.com/company/code-sync/ Mail: info at codesync.global #CodeMesh #Idris #EdwinBrady #TDDWhy it's here
8 people recommend thisWhat people say. Recommended as an excellent introduction to dependent types and the interactive code generation capabilities of the Idris compiler.
u/WalkerCodeRangerAdamant Languagein r/ProgrammingLanguages • Recommends
Idris 2: Type-driven development of Idris - Edwin Brady
huntieon Hacker News • Recommends
On “Dependent Haskell”
Dependent types are types which depend on values. As an example, think of the cons procedure: (List A, A) -> List A. It takes a List of A's and an A and returns a List of A's. With dependent types you can write this as (List n A, A) -> List n+1 A. This tells us that cons takes a List of A's with length n and an A returns a List of A's with length n+1. Edwin Brady shows off some examples in Idris here1. I thought the matrix example was really impressive. 1 link to this video
pezo1919on Hacker News • Recommends
On “Ask HN: What is your favorite non-generic or semi-obscure programming language?”
Idris lang seems awesome with the atom plugin. :) Did not use it yet but I hope it will get more attention. link to this video
resoluteteethon Hacker News • Recommends
On “Idris 2 programming language announced”
…d, I found the official announcement on the Idris mailing list: link He says "No doubt I'll say more about this over the next few weeks," so it sounds like he's planning on making a more detailed announcement later. Edit 2: Also, as someone who hasn't been following Blodwen or how it's different from Idris 1, this looks like a good introduction: link to this video…
still_grokkingon Hacker News • Recommends
On “Fun and dystopia with AI-based code generation using GPT-J-6B”
You don't need the tests. You need only the types. And especially you don't need "artificial dumbness", which does not understand code, and therefore won't produce correct results, but just an advanced programming language. Say hello to Idris! :-) link to this video
sourcelesson Hacker News • Recommends
On “What will programming look like in 2020? (2012)”
I don't know, some of that is at least starting to happen with Idris 2, though not in the exact way predicted: link to this video (Type Driven Development with Idris 2) Short summary of linked video: when your type system is powerful enough you can restrict the set of possible implementations to the point that the compiler can make a decent guess as to what the program should be to satisfy the type signature.
Jeff_Brownon Hacker News • Mentions
On “Reltron: a GUI for exploring relational databases”
I agree about its availability. I think it's far more useful than you seem to, though. Reducing the problem space is huge. It's why macro programming (ala Lisp) is so dangerous. It's why I left Haskell for Python, and why I often wish I was using Idris1, which pretty much reads your mind and writes what you meant. It's true of coding generally, but SQL programming especially, that there's a conceptually obvious, small space of reasonable programs, but because we're writing in text, we're free to roam over an enormous superspace of (occasionally) wrong or (usually) meaningless programs. 1 link to this video
nathcdon Hacker News • Mentions
On “Compiling Knowledge into Probabilistic Models”
> In the general-purpose programming context, imagine if you could give examples of a program output (domain data) along with a skeleton of a program (source file with incomplete parts) and ask a system to fill in the holes. This part reminds me of some of capabilities of the Idris compiler 1. In an Idris program you can leave "holes" to stand in for incomplete parts of a program 2, and the compiler can infer various bits of code from types and holes. In a demo of the in-progress Idris 2 compiler 3, Edwin Brady refers to it as a "lab assistant" and shows it writing a whole function when given a function type. 1 link 2 link 3 link to this video
rossngon Hacker News • Mentions
On “What I Want from a Type System (2016)”
Hoogle is pretty nice, and few other languages had an equivalent until quite recently. I'm hopeful that cool type-powered IDE features will start to arrive once haskell-ide-engine is a bit more stable. It's getting there! There are some pretty awesome IDE ideas in Haskell-ish languages like Idris 1, too. There is some movement towards dependent types in Haskell, so it might get similar features one day. 1 link to this video
T-Ron Hacker News • Mentions
On “Modern SAT solvers: fast, neat and underused”
SAT solvers are starting to be used as tooling for functional languages - Liquid Haskell uses one for refinement types1, and Djinn uses one for suggesting functions given a type2. Similarly to Djinn, Edwin Brady gave a presentation on using an SMT solver to do live code suggestions/implementation inference in the successor to Idris3. 1 link 2 link 3 link to this video
jbjohnson Hacker News • Mentions
On “Hazel: A live functional programming environment featuring typed holes”
Interesting. I didn't notice any reference to Idris 1 but that was the first place I saw this style of development. 1 link to this video
dietr1chon Hacker News • Mentions
On “What would it take to add refinement types to Rust?”
Refinements embed a predicate that elements of the new type must pass. def Nat = Int: (|x| -> x >= 0) Dependent types allow types to be computed from functions (and depend on arguments, otherwise it seems they become just weird constants), def Five(as_type: String) -> NumericType(as_type): match as_type: "string" => "five" "int" => 5 "float" => 5.0f "double" => 5.0d _ => panic() // Unnecessary if you refine `as_type` from a String to an enum or a fixed set of strings. Dependent types seem weird, but they help making types first-class ( link to this video ) and gaining types like `Array<T, N>` that allow ensuring things are the right length, and define append/extend properly.