Eliminating Run-Time Errors with Agda - Computerphile

[@nilstrieb]

For those asking how this works with numbers that are, for example, input by the user: The type of these number will just be a Natural number, so you can't use these to index the Vector. There is a function that can convert your Natural number into a Fin, which you'll have to use, and that function returns a Maybe Fin, so you'll have to explicitly handle that case, which is what these languages are so strong in.

[@felixthehuman]

So what you're saying is that even though the error happens while the program is running, it happens while program is compiling the user input, before it ever tries to run the users input?

[@nilstrieb]

@@felixthehuman It's not really an "error", it's just another code path. Your program won't crash, and it will never crash, which it absolutely can in languages that don't work like this.

[@TheJamesM]

@@felixthehuman I think one way you could put it is that there's no undefined behaviour. For it to be a valid program every potential state has to be accounted for. (Though I don't know how this is affected by memory limitations, hardware failure, etc.)

[@chriswarburton4296]

@@felixthehuman I wouldn't use the phrases "compile" and "run", since those have different meanings; I would say we *parse* the user's input. In fact, we would probably parse it in two steps: to look up a user-provided index in a vector of, say, 100 elements, we would first parse the user's input from `ByteString` to `Maybe Natural`. This step might fail, since the user might write something that doesn't make sense as a number, like "hello". Once we've got that Natural number, we would parse it to a `Maybe (Fin 100)`. This second step might fail, since the user might write a number that's not in range, like 123. Pretty much all programming languages force us (via types) to do that first parsing step, from ByteString to number (although they often use `int`, which is very dangerous since it would allows negative indices!); most languages don't use types to force us to do the second step. That's because their type systems can't represent types like `Vec` or `Fin`. Agda has much more expressive types, so we can use them to make sure the correct checks are performed.

[@chriswarburton4296]

@@TheJamesM Unfortunately, trying to handle out-of-memory would make life so uncomfortable that it's usually assumed we have infinite memory (and throw an asynchronous exception if we ever hit OOM)

[@InspektorDreyfus]

Naming a list l1 is the 11th worst mistake to make.

[@TheVergile]

this implies there is a list…

[@kamilziemian995]

I agree.

[@amigalemming]

Naming is much more difficult than proving correctness of a program.

[@chriswarburton4296]

A good example of how this can get difficult is if we change the type of vector append (++v), so instead of returning a vector of length "m + n", it instead returns a vector of length "n + m" (i.e. we add the lengths the other way around). This shouldn't change anything about the program, but now we have to prove to the compiler that adding natural numbers is commutative!

[@pooroldnostradamus]

*refl intensifies*

[@brentknight9318]

It took me 10+ years to realize that exceptions are terrible. Golang’s explicit error-checking with multiple return values (plus defer, panic, recover) is honestly the best balance I’ve seen in ~40 years of programming

[@eyemotif]

so the opposite of javascript?

[@inderjeet8659]

loool

[@nodroGnotlrahC]

To everyone saying "what's the point?" I'm not in Safety Critical Systems, but I've hung out with people who are, and they explained it like this. You know how every OS, every compiler, every app, has pages of terms and conditions that boil down to "if our software f***s up, that's your problem, not ours" and you click the OK button without reading it. Someone who is building a nuclear reactor of a fly-by-wire plane will NOT agree to that. They will insist on Ts&Cs that say "if this software crashes at runtime and causes another Chernobyl, or drops a plane onto a city, I will accept full responsibility and I understand the consequences will be severe". (And don't bother trying to get insurance against that, no insurance company will touch you with a barge pole. It will be on YOU.) This is why you really want a system that is proved will never crash because of, for example, an array bounds error. And by proved I mean mathematically proved, like it has been proved that you can colour /any/ map with four colours. Not "we tried a whole bunch of possibilities and didn't find any five coloured maps" or "we ran a billion simulations and they were fine, plus we reviewed the code really carefully and didn't see any bugs" . That's not proof.

[@twistedbydsign99]

Better to have a programming language that blows up all the time and you learn to deal with it and monitor, than a programming language that never blows up except that time it does and everyone shits their pants.

[@willful759]

@@twistedbydsign99 so you rather have airplanes crashing all the time on cities and have a wonderful learning experience about how to fix that bug? I understand what you mean, but I think you didn't understand the point op was making

[@johanliebert8544]

@@twistedbydsign99 Not every program is written for GUI, Web application, etc., where you can live with crashes. Some applications cannot afford runtime mistakes. What do you suggest should one do in case of, say an aeroplane code? I work in ASIC industry. We too cannot afford to have "runtime" mistakes, which basically means you have to rebuild the chip. While we don't use any mathematically proven languages, we write an extremely large number of test cases, formal/functional verification, which are also aided by different coverage checks. Even with all these checks in places, few errors still leak out and we'll have to end up patching them up (most of the time by a software patch, sometimes by turning off a feature, etc). Just because you work with systems that can afford mistakes, not everyone can.

[@laz001]

How is it even possible to create software that doesn’t crash, when the hardware below it can crash - at an assembly level.

[@nosenseofhumor1]

yeah but not crashing != bug free. it does feel like we have just moved the problem a little bit

[@tokenr7414]

Agda eliminates runtime errors by eliminating noob developers, who are not insane enough to learn such a difficult syntax :)

[@delphie23]

The syntax actually makes a lot of sense but it takes time to get used to. For example the use of a colon (:) to denote typing and arrows (->) to denote functions is very common in mathematics (for example you denote a function 'f' from A to B with "f : A -> B"). The use of spaces for functions application is very common in functional programming and it's done to cleanly support currying and partial application. However - the use of operator symbols instead of function names is indeed very controversial and is probably done mostly to appeal to mathematicians. That is not to say Agda isn't a difficult language, because it definitely is, but its difficulty comes from its ability to do things very few languages can like proving theorems and enforcing properties of programs. The syntax is the easy part.

[@mauricio0guaruja]

hahahahahaahah

[@LazieKat]

just and nothing sound like Some and None enums in Rust, which I really love

[@chriswarburton4296]

Yep, ML uses the names Some and None, and its descendents like Rust and Scala use those. Haskell (which is also a descendent of ML!) chose to call them Just and Nothing, and Agda descends from Haskell.

[@hansisbrucker813]

You might like languages like Haskell and F# too. 😊

[@tervaaku]

Rust is basically C trying it's best to be to be OCaml pretending to be C++. Functional features without functional clout, but still no monads ;-;. highly based though

[@delphie23]

@@tervaaku Rust has monads, even Java has monads. What Rust lacks is higher kinded polymorphism, which makes it a bit easier to work with monads - so you have monads but you don't have "Monad" as a trait, so you can't really generalize over monads and you often have to duplicate code when using them.

[@Jasruler]

@@hansisbrucker813 f# is great.

[@sheevys]

Let's do Idris next!

[@damiensadventure]

Idris and his body double are immune to "run time" errors. Nothing goes short or long with Idris. Just smooth and clean operation. Jk Idris would be be neat

[@Madsy9]

Please do the Idris programming language next. It even uses Martin-Löf type theory as a part of its type system :-)

[@ivypierlot]

but agda is better because it can do cubical type theory

[@polendri4812]

@@ivypierlot And Idris has quantitative types while AFAIK Agda does not. See how unhelpful it is to be calling one language "better" than another based on one feature?

[@bram9762]

@@ivypierlot What use is cubical type theory for programming?

[@bram9762]

@@polendri4812 Agda has erasure annotations based on qtt but no linear functions

[@delphie23]

@@bram9762 Mostly the ability to declare separate terms in a type as equal (using higher inductive types) in such a way that all the functions from that type would have to respect those equalities. So for example you can define rational numbers as a quotient of pairs of integers in such a way that two different pairs of numerator and denominator who denote the same rational number (that is - they both give the same reduced fraction when divided by their greatest common divisor) will have to be treated as equal by all functions when interpreted as terms in the type of rational numbers, so you can't accidentally create a function which tells them apart (for example by returning "true" when it gets r(4,8) and "false" when it gets r(1,2)).

[@nilstrieb]

I've been trying out Idris recently, dependently typed languages are indeed very interesting!

[@benjaminflin5183]

Idris 2 has quantitative type theory which lets you reason about which values are kept at runtime. Very useful when you want a compile time proof that doesn't harm performance at runtime. Also linear types are cool!

[@wbfaulk]

"This language cannot produce runtime errors." "What about these errors that happen at runtime?" "Those aren't the runtime errors you're looking for."

[@ICopiedJohnOswald]

That was a compile time error not a runtime error.

[@Stierguy1]

I've known this topic by the name "behavedness proof by typing". It is my opinion that a modern programming language should not introduce undefined behavior or dynamic errors into its design without also providing sufficient typing to make them into static errors where not otherwise indicated. A type system can also carry correctness proof, i.e. proof that the program and a given operational semantics are equal (in various capacities). These are fundamental pursuits in the modern design of systems languages too, not just academic and research languages.

[@johnredberg]

It seems that all this is doing is abstracting run-time errors away from the programs and moving them straight into the developers' brains.

[@GordonjSmith1]

Which is perhaps where they should be! That is potentially why software engineers are NOT qualified as professional Engineers with the equivalent status in society as a 'Professional' (PS I wrote my thesis on it, just walk on past).

[@Chase-up3do]

It's embedding runtime errors into a strong compile time type system. It has been proven time and time again through years of research that a strong type system is the most consistent program correctness checker. A theorem prover, really. Why not use it to the fullest? If we can have mathematical guarantees about the run time....during the compile time - well that sounds like a super power, give me the entire stock please!

[@pladimir_vutin]

@@GordonjSmith1 You mean software engineers are not seen and creditted as real engineers in society bc of how they handle errors or bc they don't take themselves seriously? Could you clarify more? I'm a bit confused by the word " qualify " , they seem to be doing ok. I mean sure, 80/100 plus are just copy paste clowns , but still the work gets done

[@sarajohnsson4979]

To me it's kind of the opposite. Yes, type checking forces you to think about what could go wrong, but you should've been doing that already. The difference is that by making you do that in a structured way, you can then take those assumptions you made and throw them at the compiler and go "hey, computer, check that this is all valid and works" and the computer will just... do that. Given a problem, a computer can't come up with a solution because it's only slightly smarter than the average brick, but given a solution it can verify it quickly and in great detail. Humans are the other way around - we're creative but we tend to overlook things and miss edge cases. So we can let computers do what they do well, and we get to spend our time doing what we do well instead And the more flexible your type system, the clearer you can be about what is or isn't correct behaviour. Want to tell the compiler to yell at you if you add some new option but forget to update the help text? You can!

[@recompile]

@@Chase-up3do Not really. A strong type system will catch exactly one class of error -- type errors. Type errors are surprisingly uncommon. This is just like the silly claim that using dependent types eliminates runtime errors. This may prevent a particular class of errors, but in no way eliminates all runtime errors.

[@Spikeypup]

I really wanted to understand this so much more than I was able to, honestly the accent, it was too much for me to try to filter, I would be trying to just understand literally what he said, and then concepts were moving on while I was still just processing the language, I don't know about you but when I'm trying to learn something new I ultimately end up failing if I can't understand what the instructor is saying. And before anyone says Closed Captions... yeah, go ahead and turn them on, read what comes out. The AI was just as confused as I was. Anyway, thanks for trying, love the channel! :)

[@legotechnic27]

Does professor Thorsten Altenkirch know anything about Dafny? It's also a language designed to allow correctness proving, but based on the more common imperative programming style. Not having used much functional programming myself, I would really like to hear the pros and cons of Agda vs Dafny.

[@kamilziemian995]

I need to watch more Thorsten Altenkirch videos. His talks are so interesting.

[@hadawaycolton4263]

i love how hard captions struggle to understand this guys accent.

[@controlflow89]

In practical programming lists of known size are rare comparing to variable-sized data structures. I wonder what Agda can proof around vectors of length n, requesting more content on Agda/Coq/Idris!

[@okuno54]

Something already shown here is variables used to index a list. One could write (I'm not familiar with Adga specifically, so "something like") a function that reads a number as user input, then creates a list of the numbers from zero up to the user's number, and another list of exactly the user's number of ones. The compiler won't know exactly what size either of those lists are, but it _will_ know that the two lists have the same size, which means you could pass them both to a zip function. Perhaps not a useful application, but it does show how unknown-length lists aren't a big deal.

[@chriswarburton4296]

@@okuno54 Exactly right. Here's some rough code for that (untested ;) ) -- Parse user input to an unbounded Nat stringToNat: String -> Maybe Nat stringToNat [] = Nothing stringToNat (x::xs) = case stringToNat xs of Nothing -> parsed Just n -> case parsed of Just m -> m * 10 + n Nothing -> Nothing where parsed = case x of '0' -> Just 0 '1' -> Just 1 '2' -> Just 2 '3' -> Just 3 '4' -> Just 4 '5' -> Just 5 '6' -> Just 6 '7' -> Just 7 '8' -> Just 8 '9' -> Just 9 _ -> Nothing -- Counts up to one-less-than the given Nat upTo: (n: Nat) -> Vec n Nat upTo zero = [] upTo (succ n) = n :: upTo n -- List of ones of the given length onesOf: (n: Nat) -> Vec n Nat onesOf zero = [] onesOf (succ n) = 1 :: onesOf n -- Combine two lists pair-wise zip: Vec n a -> Vec n b -> Vec n (a + b) zip [] [] = [] zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys userInputToZippedLists: String -> Maybe (Vec n (Nat, Nat)) userInputToZippedLists str = case stringToNat str of Nothing -> Nothing Just n -> Just (zip (upTo n) (onesOf n))

[@Bratjuuc]

@@chriswarburton4296 I believe Agda's "where" syntax differs from Haskell's one, but I don't remember if that is a 100% truth

[@tervaaku]

Assuming single-threadedness and infinite memory, it's safe to have an array store it's own length at runtime (give or take implementation details), so you can have variable or even dynamically sized types as long as you restrict access to them by something that forces error checking like Result or Option/Maybe

[@chriswarburton4296]

@@Bratjuuc Probably; I've not actually written any Agda in a couple of years ;)

[@moritzschmidt6791]

This looks and feels so much like Haskell. I understand it, but I dont really get it.

[@bimsherwood7006]

Like haskell, but you can define types in terms of data? It always bothered me that you couldn't define matrices in haskell and put the dimension in the type. But it looks easy in agda.

[@cajunvoodoo5930]

@@bimsherwood7006 check out the `massiv` library. it does what you want and more. its also stupidly fast

[@MOAB_MOAB]

Well maybe we can help each other out here: I really get it, but I don't understand it. You start. Help me to understand it. And then I'll help you get it. Get it?

[@cajunvoodoo5930]

On second thought you may not have been replying to me. KZbin shouldn't have notified me

[@Rastafa469]

@@bimsherwood7006 "It always bothered me that you couldn't define matrices in haskell and put the dimension in the type" Actually you can it's just not as "first-class" as in agda. Lookup "Haskell type level programming"

[@Bit-while_going]

Not a bad educational tool, and looks useful as well. Looks like it takes a skilled worker, a specialist. Probably a good skill to have.

[@InShadowsLinger]

I have watched this three times now and I still have hard time understanding everything that is going on in here. I mean, I understand what he is saying and what the code is supposed to do, but I am not able to match it with the syntax. What is the F in 0F and 1F? I pretty much don't understand the entire line suc : ( i : Fin n) -> Fin (suc n). Everything I can find on Agda jumps over the basics and assumes that the syntax it understood. One of the most frustrating videos from computerphile for me.

[@Bratjuuc]

I believe F means "this number belongs to Fin n type for some natural n" (i : Fin n) -> Fin (suc n) is the type signature of the FS constructor. It means "for any natural number n, it recieves any element of type Fin n, namely i, and returns an element of type Fin (suc n), where "suc" is just a constructor of Nat type. Suc n basically means 1+n. Writing (i : Fin n) instead of Fin n is redundant in this case, because i was never used.

[@JamezMartinez]

give me the zucc

[@nodroGnotlrahC]

So, to clarify, would I be correct to assert that you cannot code the Collatz conjecture in Agda? e.g. a function that returns the length of the hailstone sequence for n because it has not been proved that this function will terminate?

[@gogich]

Agda (just like any turing complete programming language one can conceive) can't possibly solve the halting problem.

[@Schnorzel1337]

What saba wants to say: no you can write any program you want, that is not easily proven to never terminate, so simple infinite recursion for example is of the table.

[@capability-snob]

@@gogich Agda is not turing complete, it's total. It turns out that this is not a problem for most practical programs.

[@Axman6]

Of course you can, you just have to prove the termination of the Collatz sequence for all integers to the compiler; Simple! 😅

[@nodroGnotlrahC]

​@@Axman6 Oh, that's alright then, because I have discovered a truly remarkable proof of this theorem which this youtube comment is too small to contain.

[@AndrewFRC135]

It's interesting to learn about these very high level and abstract programming languages. I primarily develop for microcontroller embedded systems written in C, so the translation from source code to metal is obvious. I am not sure how code written in Agda and other simmilar languages are compiled into machine code, or if there is always an interpreter involved somewhere.

[@Axman6]

Also you might find the seL4 project interesting, it was formally verified in Isabelle HOL, a roughly equivalent dependent lot typed language, which was then translated into Haskell, with proofs of that translation maintaining semantics, and then translated into C, again proving the transformation. IIRC, it is also proven correct down to the produced assembly these days but don’t take my word for it.

[@jakesecondname2462]

@@Axman6 Isabelle/HOL isn't dependently typed, but yes.

[@frognik79]

But can it compile Crysis?

[@recklessroges]

No because Crysis is written in C++, (and is full of hacks and bugs that Agda won't accept.)

[@adia.413]

​@@recklessroges hahahaha, at least C++ is widely used.

[@emiflake]

Oh wow, comments are a mess, looks like the Computerphile audience isn't quite ready for actual computer science huh

[@alkouille2794]

it's astouding how people are proud to be ignorant

[@recklessroges]

The problem with "giving people what they want" is that they ask for what they /think/ they want, (which isn't the same thing.) I enjoyed this episode. Nice and Haskelly.

[@Nors2Ka]

Ah yes, I remember the part in the video where they did some rigorous science. That's something I can't handle!

[@emilioschmidt2106]

7:49 just a casual "naja" in there

[@SimGunther]

If only this had a more pretty & straightforward syntax :)

[@snoopyrobot5993]

to each their own I think it looks wonderful

[@harry3life]

Hmm? I thought this syntax was about as clear as could be. Much better then most languages like python, js and C#.

[@nerkulec]

I think the syntax is pretty clear, it looks just like haskell

[@alphaprimal1669]

this syntax is cool, haskell like and readable, if u prefer ML like syntax give F* a read (it's still in dev phase tho)

[@DonGioification]

I agree, the syntax is absolutely horrible

[@pmcate2]

I don’t get it.

[@northcode_]

Hes showing a functional programming language called agda, and how it uses its type-system to be able to check at compile time that your program can't crash at runtime. Its doing this by making you define what should happen for all cases, and then when you happen upon a case what you can't implement, you know it wouldn't be valid. You see this in his list index example, where he starts implementing the index operator for lists and agda says "you have to implement this for the empty list" and since theres no way to implement it he has to introduce the 'Maybe' return. This way you wouldn't get a runtime error saying something list "list index out of bounds", it tells you at compile time that there can be an error here and you have to deal with it.

[@amigalemming]

Can I also have an access function with a type like: _!!_ : List A -> (N : N < length (List A)) -> A ?

[@artemiasthegreatest]

Best language ever! Was my first language with dependent types... Such a beautiful and simple mixfix notations... I am so tired by now of languages and languages embedded into Coq to achieve same goals.....

[@Belioyt]

Can Agda be used to build real world software? It looks to me to be a tool for compsci undergrads or those doing research in compsci.

[@冥-m2q]

@@Belioyt Not in the sense that Haskell does. You can use Agda to formally verify certain parts of your system then have that translated into Haskell. Particularly useful for stuff like cryptography, really, but impractical on domains beyond those requiring proofs.

[@007drak007]

@@Belioyt Hell no, even new languages are still pushed back by old ones. None will use this for commercial use. None.

[@RupertBruce]

The constraints imposed by JPL were interesting (eg. No malloc)

[@Axman6]

This is really common in the high assurance systems world - Ada’s Ravenscar profile is for exactly these sorts of systems, it prevents all dynamic allocation, and the only tasks which are allowed to execute are ones which can initialise all their resources at launch, and must then be comprised of a loop which never terminates.

[@123TeeMee]

This is actually quite interesting, perhaps my computer science knowledge won't be useless after all!

[@mlguy8376]

Just speak to me - I write perfect code one time, every time! If there is a “bug” it is a feature ;).

[@davidgillies620]

A lot of these compile-time guarantees are the motivation behind Rust. It's not as strict as this, but it does make writing dangerous code a lot more difficult (it also makes writing code that does anything useful more difficult, but them's the breaks).

[@ccgarciab]

Ye, but there are so many utility functions and sugars that it almost evens out. Almost.

[@bonononchev634]

Kinda, if you mean concerning memory allocation, which is a major PITA for C/C++ - like half your development effort is debugging memory allocation crashes… Still worse than GC though … which Rust avoided in order to integrate better with C/C++ code.

[@davidgillies620]

@@bonononchev634 I haven't had a memory allocation problem with C++ in ages. The RAII semantics you get with things like std::unique_ptr and std::shared_ptr abstract away almost all your concerns with object lifecycles. I almost never invoke new and delete these days. The compiler can detect most instances of aliasing etc. and either warn you or fail to compile.

[@embeddor2230]

Such static checks can be easily implemented with the C++ template system and constexpr evaluation.

[@josephlunderville3195]

Is there some way the type system itself is actually richer than Rust or Haskell or C++? Or is this about convenience and syntax?

[@embeddor2230]

@@josephlunderville3195 I don't know much about this language, but my guess would be no. I think Agda is one of those languages that are just for research and theoretical purposes.

[@guiorgy]

This strongly reminds me of Haskell.

[@cajunvoodoo5930]

it descends from haskell actually! but its not nearly as powerful

[@perigord6281]

The compiler is also written in Haskell.

[@hobrin4242]

But what if you input an unproofed mathematical statement, and the program crashes depending on if it is true or not?

[@KManAbout]

That's what this language is for. It won't crash it'll just be a nothing.

[@TheMisterGege1]

How would it work when we created the vector at runtime but hardcode an index? Let’s say we download a file with 10 entries and create a vector that contains each entry of the file. And sine we ‘know’ the list always has 10 entries we have a function that accesses the entry at index 9. Ho can we prove to the compiler that this is correct? And what happens if someone changes the remote file and it now only has five wntries?

[@冥-m2q]

You can solve that by having some routine return `Some` value or `None`.

[@bonononchev634]

Well that is the point - the indexing function is not “List A n -> Fin A m -> A” but “List A n -> Fin A n -> A”. If you have a fixed index in mind during the compilation, you can’t have a List n. In practice what you do is convert that index into a Fin 9, which operation returns a Maybe Fin n - it is either nothing if the n

[@hashiromer7668]

What is precisely meant by a guarantee that a runtime error will not occur as in if that is a proof that our program will not crash while running, there must be underlying assumptions or premises for that proof to work. For example, we know that if the hardware malfunctions for some reason, our program would crash regardless of any guarantee provided on the software level. I am interested in exploring these kind of constraints under which it is proven that runtime errors won't occur.

[@lordcirth]

Runtime crashes will not occur if the program is executed by correctly working hardware, for all possible inputs. Sure, a CPU or RAM failure can still crash it, but that's fundamentally unsolvable by pure software - you would need multiple computers running in parallel and comparing answers, like the Shuttle did.

[@dk6024]

Agda programs are guaranteed to terminate?

[@chriswarburton4296]

It uses "sized types"; roughly speaking, we're only allowed to do recursion if Agda can see that the argument is getting smaller. Notice that in these examples, the recursion is always happening on a 'smaller part' of the argument, e.g. 'f (x :: xs)' is allowed to recurse like 'f xs', but not 'f someRandomThing'. Agda also allows co-termination, which lets us write infinite loops which are guaranteed to produce output in finite time, e.g. a server which keeps running forever, but each response must be produced in a finite time.

[@marcthatcher]

@@chriswarburton4296 so it's not Turing complete buy whether that's a practical restriction or not is another question

[@chriswarburton4296]

@@marcthatcher Exactly. Note that it's *almost* Turing-complete, since we can run any Turing machine; e.g. the following type represents the steps taken, as an infinite list: record TuringMachine (states : Nat) : Set where coinductive field state : Fin states step : TuringMachine states We can, for example, count how many steps it takes for a TuringMachine to halt: stepsTaken : TuringMachine states -> CoNat stepsTaken t = case (state t == state (step t)) of True -> zero False -> succ (stepsTaken (step t)) Note that this isn't a normal Natural number type; it's a co-inductive version, which could be infinite (succ (succ (succ ...))). Once we introduce such potentially-infinite types in Agda, everything that (co-)recurses on them must also be potentially-infinite.

[@MCRuCr]

In type theory, every mathematical proof is equivalent to a type. If elements of such type are computable, the proposition holds. Now my question is: What does the type of natural numbers proof? That natural numbers exist?

[@karthikravikanti]

My understanding is that that "types are propositions" is _an_ interpretation of a what a type is. The other more common interpretation is that it's a set of values, which is what the type of natural numbers would be. So, not all types are propositions, but if you want to force that interpretation, I suppose yes, the type of natural numbers is a proposition that natural numbers _are_.

[@ThorstenAltenkirch]

You start with a proposition and construct a type of it’s evidence. But you are right nowadays we only consider types with at most one element as propositions- in this sense natural numbers are not propositions.

[@koenpauwels9617]

The way I understand it (and to be clear I'm not an expert on type theory) is that in type theory, proofs are mathematical objects that the theory itself can talk about. In everyday mathematics, we're usually not very interested in proofs as mathematical objects. In particular, we tend to treat two proofs of the same proposition as interchangeable, perhaps even identical. Type theory doesn't make this assumption: two proofs (terms) of the same proposition (type) are not necessarily the same, they may be distinct objects. (Also, note that it is not the case that proofs are equivalent to types: propositions map onto types, and proofs map onto terms). So what does that mean for the type of natural numbers? Well, let's take a look at the simplest mathematical proposition: "true", the proposition that is, by definition, true. In type theory, the simplest type that represents that often called "Unit", the type that has by definition precisely one inhabitant. In Agda you'd write "data Unit : Set where unit : Unit". Here "Unit" is the type that corresponds to the proposition "true", and "unit" is the proof (the proof that "true is true", if you will :)). But there are more types that correspond to the proposition "true". For instance, we can define a type that corresponds to the proposition "true", but that has *two distinct proofs*. In programming, we tend to call that type "Bool": data Bool : Set where t : Bool f : Bool Here "Bool" *also* corresponds to the proposition "true", and "t" and "f" are both distinct proofs of Bool. And we can, of course make a type that corresponds to "true" but which has three distinct proofs, or four, or five, ... The type of natural numbers also corresponds to the proposition "true", it just has infinitely many distinct proofs!

[@SimonBuchanNz]

@@koenpauwels9617 it's more than a little confusing to use booleans as an example of a true proposition 😉

[@holgerrodriguez9435]

Isn’t Ada/SPARK not close enough?

[@Axman6]

Similar problem domains, very different approaches.

[@DonGioification]

Why does this professor look and sound like Dave grohl and Arnold Schwarzenegger had a child

[@BooBaddyBig]

Right, so what you're saying is that I can download my tower of hanoi program to a nuclear power plant and it will work correctly because it's type safe!

[@barmetler]

template A get(const std::array &as) { return as.at(index); }

[@embeddor2230]

C++ had constexpr evalutation for ages. Presenting such a feature as new and exclusive to agda is kinda misleading imo.

[@perigord6281]

It is limited to literal types though.

[@barmetler]

@@perigord6281 you mean agda? Because my comment isnt, i tried it

[@perigord6281]

I meant C++

[@barmetler]

@@perigord6281 you can do calculations at compile time with all things that are of a "literal" type, meaning constexpr constructor and destructor

[@robertsemmler8272]

I have so much respect for that guy, but he s using a mac?

[@toddmarshall7573]

2:21 What character set has a left or right pointing arrow?

[@reecemcmillin6570]

I don’t want to make claims about his exact font, but any monospace with ligatures should cover it!

[@okuno54]

Well, the character set is Unicode, but plenty of other character sets define arrows e.g. the Atari ST character set (which was the first weirdo to include them when I browsed on wikipedia a bit). What font has arrows? Well, lots and lots of them. Adobe Source Code Pro has some ugly arrows; Computer Modern (the default LaTeX font) has some nice-looking arrows which unfortunately aren't monospace; the DejaVu family has them; the list goes on for ages. What input method allows you to input arrows and other special symbols (i.e. "how")? Well, Emacs is a fully programmable editor: as I understand it, there's a plugin for Agda which will recognize sequences of ascii like "->" or " at" (I'm kinda just guessing what the actual sequences are) and replace them with the Unicode equivalents. I don't personally use Emacs though; for when I need special symbols, I've configured my OS to use a compose key (symbolized ⎄). If I type "⎄->", I get →; to get ℕ I type "⎄bbN". I've got hundreds of these sequences for mathematical letters/operators, most of the international phonetic alphabet, and a few fun ones 🖖 (´・ω・)っ由 at my fingertips. There are other ways to get the same effect (custom input method software, probably easier to just use autohotkey on Windows), and if you can be bothered to memorize (blegh) the unicode assignments you can use always use alt-codes.

[@wbfaulk]

More to the point, which keyboard has one? You can see him enter one at 6:09. It looks like a trigraph, which seems inconvenient. The Agda docs say it's entered with " -". And "ℕ" is "\bN". Also, the "∷" apparently isn't two colons, but the single Unicode character "PROPORTION" at U+2237, entered into Emacs with "\::".

[@isbestlizard]

YES I like the feels of this language if you're designing a nuclear reactor control system definitely use this not Python or Javascript

[@SharienGaming]

there is just one issue - if every program in this language is guaranteed to terminate...it is never suitable to run anything... because control programs need to run indefinitely - they are constantly monitoring states... they inherently are "may terminate, but could run indefinitely" programs - which if i understood this video correctly...these cant be some components could be built using something like this - but not the whole thing mind you... no one is crazy enough to write something like that in javascript - way too much undefined behaviour

[@johnbennett1465]

Assuming that the claim that all Agda programs terminate is correct, then it is NOT Turing complete. I.e. it is a special purpose language. Without a clear statement of what problem domain it is intended to address it is impossible to evaluate the language.

[@jakesecondname2462]

Look up the CS stackexchange question "Can one get Turing-completeness without nontermination?" and similar.

[@cazino4]

That was exactly my thoughts, I said as much in my comment too.

[@ThorstenAltenkirch]

Not really an issue: you can represent any program using the partiality monad which you can use to reason about potentially non-terminating programs at compile time but just run them at runtime.

[@johnbennett1465]

@@ThorstenAltenkirch certainly it is possible to prove that some programs halt. Doing so can be useful. A tool would ideally return which combination of will halt, will not halt and undecideble applies to a program. Along with the conditions that cause each. So what advantages does this approach have compared to others? I have heard of a number of approaches to proving correctness of programs over the years, but I have not looked closely at any of them.

[@ThorstenAltenkirch]

@@johnbennett1465 There will be another video soon where I talk about proving properties in Agda, maybe this addresses your questions. In a nutshell: a language like Agda already comes with its own logic for free by assigning types to propositions and representing proofs as programs. In reality the border between logic and programs is fluid and it is advantageous to have a language that supports moving between these realms.

[@JohnDavidDunlap]

How does agda prevent divide by zero errors at compile time?

[@northcode_]

You could do this either by defining division as Nat -> NonZero -> Nat, so you can't use division without converting your input to NonZero, which would require checking if its zero. Or you could make division return Maybe. I haven't looked that much into it, as this video is the first time I'm seeing agda, but from what little I've read it seems its doing something like the first approach. With similar implementations for floats.

[@JohnDavidDunlap]

@@northcode_ I was afraid you'd say that. divide by zero is one of those runtime errors that I don't think it's possible to solve at compile time.

[@northcode_]

​@@JohnDavidDunlap well, depends on how define "solve". Using the first method makes it impossible to write a program that can divide by zero. So anywhere you try to divide anything that COULD be a zero, it will not compile, you'd have to explicitly check that it is not zero first by converting it to a NonZero. Probably through some Nat -> Maybe NonZero function. Of course theres no way to guarantee that you don't divide by zero for any user input, because then you wouldn't be able to accept any user input. I mean if the variable is dynamic at some point you have to check that its not zero. In C, if you divide by zero, the cpu will check it for you and throw a trap signal that the kernel turns into a runtime error, unless you remember to add the if (dividend != 0) before doing the division yourself, in which case the 'else' branch is your 'runtime error'. The thinking of agda and a lot of functional languages is to move as much of these checks to the typesystem as possible. So that there is no way to forget to add the 'if (dividend != 0)' check. This way it forces you to do these checks, and you write better and safer programs.

[@chriswarburton4296]

We can use a type like this: data NonZero : Set where succ : Nat -> NonZero The only way to construct a NonZero value is to take the successor of a Natural number; that can never be zero. If we use this type for our denominator, we guarantee no divide-by-zero errors. Note that we can easily represent negatives, using a type with two constructors, e.g. `+succ_: Nat -> NonZeroWIthNegatives` and `-succ_: Nat -> NonZeroWithNegatives`. We can represent fractions as ratios, like `_/_ : Nat -> NonZeroWithNegatives -> Ratio`

[@chriswarburton4296]

@@northcode_ The difference between the two approaches is that when we use Maybe, we always forced to deal with the Nothing branch; even if we're sure it will be non-zero. The NonZero approach gives us the opportunity to tell the compiler. I don't do much division, but I often use modulo to pick an element from a NonEmptyList. Note that a `NonEmptyList t` is just a tuple of `(t, List t)`, and its length is NonZero. Hence we can write a function which looks up any Natural number in a NonEmptyList, by using `length : NonEmptyList -> NonZero` and `modulo : Natural -> NonZero -> Natural`. This doesn't need any runtime checks, and has no error/unhandled branches.

[@brunogrieco5146]

What happens when you ask the user to input the desired location, and it is out of range? I imagine that there would be a lot of maybes and justs in between...

[@sarajohnsson4979]

What happens when you ask the user to input the desired location, and they type "cheese"? "4" isn't any more useful than "cheese" if what you need is a location in the list `[1,2,3]`, is it? Why is checking for one of those fine but checking for the other a problem? Shouldn't you be checking your inputs for *any* program written in *any* language?

[@Stierguy1]

@@sarajohnsson4979 The idea here is that once you check your `string` it's no longer just `string` but actually `"this"|"that"|"those"`, otherwise the input is rejected and the program follows the correct control path to handle that situation. This is what constitutes a well behaved program. The type system lets us actually be sure that the control path which accepts the input will never handle an unacceptable one, or mishandle an acceptable one.

[@Verrisin]

EDIT: yaay, he talks about it right after :D (of course - I always comment too soon :D) 9:18 - ugh, just a Maybe? I was hoping for something smarter, since it's a solver, like `uncompilable` and then, each time I write `x !! 4` if it cannot check that x will have at least 4 elements, the program will not compile at all - Explicit is a bit better than just throwing, but you could just have explicit throwing instead, which would automatically propagate, and when calling a function show you all possible ways it can fail, for you to handle at any point above in the "call stack" etc.... (and of course, `main` or `IO` cannot have any uncaught errors) - I expected something smart from Agda ... ... oh well, video is not over, maybe I will still be surprised...

[@willful759]

well this is a small demonstration meant to be quick and easy to understand and people are already rioting about how useless and nedlessly confusing all of this is, probably you can do all that in agda but that would probably make for a longer video and even more people rioting

[@Salsuero]

I hate programming languages that use characters that aren't on my keyboard. I don't wanna have to use special function keys or copy/paste methods just to input a right arrow character.

[@glesmord]

The auto generated captions are having a bad time

[@jasenq6986]

Really like agda

[@esquire5978]

“We took a computer…”

[@geonerd]

Ada's long lost sister?

[@Axman6]

Ada approaches correctness from a very different perspective, everything down in this video can be defined by the user, in the language itself, and you essentially teach the compiler how to prove things correct. Ada is somewhat more limited, and somewhat clunky where you can add checks to procedures which the compiler will check as much as it can and add runtime errors if it can’t check they haven’t been violated. SPARK gets closer to this though.

[@xokyle]

neat, but who actually uses agda?

[@caseysick2154]

How many programmers out there left at 3:17?

[@Verrisin]

I've actually had an idea for a language with features like this. Mainly: User code can run both at runtime and at compile time. All compile time types are actually objects you can manipulate and compute "normally" but only available at compile time. (they _implement_ type checking rules). It would have a smart type system, that derives most things, instead of just checking... - It also has a lot of useful features, because it's meant to be practical, not academic. - I will obviously never make it (lol) but I would at least like to write a "blog post" about the ideas. I'm sure many people had them, but I liked the way I structured it. Not even the design is complete, though. It's just something I do for fun, when I'm frustrated with what I have to use. XD - Then again, AGI might happen sooner than it's done, so I kind of gave up on trying to improve anything anymore XD

[@Verrisin]

The main thing really is: having the full language available at compile time, integrated with the type system.

[@MrMomoro123]

That sounds like one of the features of dependant types (which agda does). You can use runtime values at compile time in your types.

[@SimonBuchanNz]

Sounds like you want zig.

[@Verrisin]

@@SimonBuchanNz OOOOH! Very interesting! - at first glance it seems the rest of the language is quite "usual" but it definitely has the main thing I wanted! - I'm definitely going to look at it more! Thank you!

[@bernardoborges8598]

Can someone please write subtitles for this video 😅

[@TheSpacecraftX]

Requiring the unicode symbols for sets of numbers is cursed.

[@bogdansikach7709]

Haskell, is it you?

[@kleinesfilmroellchen]

Ah yes, programming with magic incantations.

[@ccgarciab]

Also know as programming

[@adia.413]

@@ccgarciab it's programming, but it's more research stuff, I doubt it will get widely used.

[@ccgarciab]

@@adia.413 being research stuff is kind of it's thing, isn't it? Doesn't make it any less programming, or even usable. I wonder why programmers have this weird conservative streak when it comes to the main technology of their craft, lol.

[@ansismaleckis1296]

I get the point but why the fcuk the syntax of this Agda is so ridiculous? Would it be possible to create a C/C++ compiler that would serve the same role.

[@冥-m2q]

It's "ridiculous" because it derives itself from the ML family of languages. Gaining some familiarity with them should factor that out pretty quickly. Yes, it's possible but it wouldn't be as idiomatic unless you restrict C/C++ into nothing more than declarative constructs.

[@chriswarburton4296]

C/C++ are imperative languages: the "meaning" of their programs comes from what they "do" (AKA operational semantics). In contrast, programs in Agda don't "do" anything, they "are" things (AKA denotational semantics). It's hard to go from one to the other without replacing pretty much everything :) In terms of syntax, you could try making an Agda-like language with C-like syntax, but you may find pretty quickly that C's syntax is actually pretty awful. For example, here are two functions written in Agda's syntax: double: Nat -> Nat double n = n * 2 square: Nat -> Nat square n = n * n These seem pretty easy to convert to a C-style syntax: Nat double(Nat n) { return n * 2; } Nat square(Nat n) { return n * n; } What about this function? compose: (b -> c) -> (a -> b) -> a -> c compose f g x = f (g x) It's a bit trickier, since we have polymorphic types and higher-order functions. A C-like equivalent would look something like: c compose(Set a, Set b, Set c, (b -> c) f, (a -> b) g, a x) { return f(g(x)); } Now how about the following: quadruple: Nat -> Nat quadruple = compose double double fourthPower: Nat -> Nat fourthPower = compose square square If we look at their type signatures, they're the same as 'double' and 'square', but we haven't written any argument names. We could write them without argument lists, like this: (Nat -> Nat) quadruple { return compose(double, double); } (Nat -> Nat) fourthPower { return compose(square, square); } This seems a bit awkward; especially since we could just as easily define these as normal values: (Nat -> Nat) quadruple = compose(double, double); (Nat -> Nat) fourthPower = compose(square, square); Yet if we can define some of our functions like normal values, why can't we define the others that way too, e.g. (Nat -> Nat) double(n) = n * 2; (Nat -> Nat) square(n) = n * n; This is essentially the same as Agda; with a few more tweaks we'd be very similar (e.g. pattern-matching is similar to switch, etc.)

[@timonix2]

So you have replaced built in runtime errors with... user defined runtime errors. I don't see the advantage here.

[@ThorstenAltenkirch]

The difference between runtime errors and compile time errors is that the former ones one only finds when it is too late.

[@timonix2]

@@ThorstenAltenkirch You don't really seem to get away with runtime errors though. If you ask a person for an input and they type an invalid input. That's a runtime error. There is no way to stop a user from inputting invalid data during compile time. What you have seems to be a way to force the programmer to do exception handling. Every error is always caught and dealt with guaranteed.

[@ThorstenAltenkirch]

@@timonix2 true but once you have checked the validity of the input you want to make sure that there is no runtime error that has been caused by a bug in your code.

[@wbfaulk]

"This language cannot produce runtime errors." 15:31 : runtime error

[@Schnorzel1337]

Actually no. The input is "v1 !!v 1". v1 is of type vector and 1 is of type Int. The compiler is not allowing to fill the function with anything but an fin so the compilation fails.

[@wbfaulk]

@@Schnorzel1337 Generally, you don't consider compilation time to be the time at which input data is provided.

[@bingloveskoki]

@@wbfaulk It is not as a program, though. He was provided the input in the interactive environment, where you can write small programs and let them run. The program was rejected by the type checker and thus did not compile. Hence, it is not a type error. It was the interactive environment, which was running, not the program.

[@wbfaulk]

@@bingloveskoki So he wrote a program. And he ran the program. And, at the time he ran the program, it generated an error. So there was an error that happened at runtime. What shall we call such an error?

[@bingloveskoki]

@wbfaulk That's not correct. The program didn't run. It was rejected by the compiler. The interactive environment just invokes the compiler with the provided input-program. Hence the error is still a static error produced by the compiler. The interactive environment just displays the compile-time error during its run-time.

[@boy_deploy]

Even if he's explaining it I can't understand. I'm so noob

[@sirnigelcogs]

Oh yes. That's certainly a thing.

[@Pedritox0953]

Very interesting

[@yuvrajt]

Les go!

[@superhussein]

THIS GUY ON THE VIDEO IS FAIRLY STRANGE BUT THAT KIND OF STRANGENESS IS ALLOWED IN ACADEMIA

[@Stierguy1]

the fact that people think its not allowed elsewhere results in extensive mistreatment and abuse called racism

[@astroid-ws4py]

He is a cool guy as we all the programmer and software engineering community

[@Yupppi]

Absolutely hebrew to someone who doesn't know any functional language and isn't quite educated in what was happening either. Just the syntax was enough to confuse at every point. But sounded interesting.

[@otraguardia]

Nice. We can reduce runtime errors to compile time errors by compiling at runtime. It’s like magic!

[@SimGunther]

IR can be run directly in some VM during compilation and not generate a binary if the IR program fails to satisfy a condition during its run in compile time. See Jai for reference.

[@qzbnyv]

I mean yeah I wouldn’t confuse what he’s demonstrating here in an interactive REPL (where he can pass in whatever and I wouldn’t really call it “runtime”) with a complete program being compiled into a binary that won’t typecheck. i.e. he won’t be able to compile the program if he’s trying to look up the value in a vector at an index higher than the amount of elements. So no out of bounds error at runtime when someone is using the program, but just a failure to even have a program in the first place instead.

[@welltypedwitch]

Agda doesn't "compile at runtime" though...

[@amogh420]

Before watching the video: Try-catch?

[@MargeryOliver-y6h]

Heller Street

[@andresfeliperiostamayo7307]

Genius man

[@AveryShibahara-w2c]

Beier Walks

[@r3wturb0x51]

This is the language you use when too many normies have adopted c++

[@HebaruSan]

This demonstration was somewhat ill-served by using a trivial toy example. The compiler can do bounds checking easily enough because you're using constant indexes, but in a real system you would almost always access array elements with variable parameters. How would the compiler track the possible ranges that an index variable and an array's length can be when they aren't known at compile time, and more specifically the relationships between them? The C expression a[i] in principle could be evaluated for any array and any index, and to do bounds checks at compile time, the compiler would somehow have to know what they will be in advance.

[@botiolle7451]

It doesn't have to know the value of "a" or "i", it only has to know their types. It would only allow you to use a[i] if it can prove that "i" is a valid index in "a". If, for example, you ask the user for "i", you would need to handle the case of "i" being out of bounds. If you didn't, you wouldn't get a runtime error like in most languages, you would get a compile error for not handling all cases.

[@chriswarburton4296]

That's the entire point, and it's why he switched to Vec and Fin types, rather than List and Nat types. Note that in Agda, using a lowercase letter in a type is shorthand for an extra, implicit argument. If we fully-expand the type of !!v, for example, we see it has this type signature: _!!v_ : {t: Set} -> {n: Nat} -> Vec n t -> Fin n -> t The braces around {t: Set} and {n: Nat} tell Agda to infer these values from the other arguments and return-type. When we see a type like (x: y) -> z, we should interpret that mathematically as "for all values x of type y, we can return a value of type z". The key insight to understand "for all" (AKA "universal quantification") is that it's really telling us that the value is *irrelevant*: in order to type-check this, Agda will ensure our definition works *regardless* of the numbers involved (and hence, *for all* possible numbers)

[@nteasushz]

Rust in C

[@laurencevanhelsuwe3052]

Variable name l1 ???? Clearly you have never read Code Complete. ;-)

[@nenharma82]

Smells like Haskell somehow.

[@ed-ou812]

Please review Clipper

[@LeDabe]

I smell ocaml in the air

[@cajunvoodoo5930]

haskell actually! similar-ish languages, just haskell is better :3c

[@hrclful]

yeah, well, but could it print "Hello world"?

[@冥-m2q]

Why shouldn't it? ``` module Main where open import Prelude main = putStrLn "Hello, World" ```

[@G7VFY]

FORTH please, something understandable.

[@syntaxerorr]

Lets make a -> wholly different -> programming language -> cool bro.

[@bingloveskoki]

Haskell -> is -> older -> than -> Java.

[@swanandx]

What about Rust?

[@swanandx]

@@roman-fo2sk depends on things you prioritise. Every language is like a tool, some are best for their specific use case. For me, I prefer Rust.

[@swanandx]

@@roman-fo2sk GO has different purpose though, it aims to be fast for "development" , so the language itself is small and has fewer keywords. It uses garbage collector ( highly optimised ) so it can't really reach low level. Every language has trade-offs. I love Rust because it assures safety without even compromising speed. And I can also reach low level for system programming. And can build freaking fast almost anything like webserver, cli apps, almost anything. GO really can't do it as I want, but yes, it's great in its own ways 😅

[@welltypedwitch]

@@roman-fo2sk Wow, you're watching a video about a dependently typed programming language and want to convince someone that Go, a language that doesn't even have parametric polymorphism, is better... just wow

[@welltypedwitch]

Rust doesn't have dependent types, so you couldn't do this unfortunately.

[@okuno54]

What about it? I mean, there is some overlap with dependent type theory, since ownership is a small (but extremely awesome!) variation on linear types. Linear types aren't dependent types, but the same people who work on one also tend to work on the other. If you'd like to see the power of both Agda and Rust combined, check out Idris 2. It's based on dependent type theory, but it also has linear types and guaranteed-compiletime-only types (which is what draws be to it).

[@Ashnurazg]

Adga is 22 years old and I never heard about it. It's a programming language that's good to proof that you have written a program that terminates correctly for some toy problems, but it's not for every day usage

[@chriswarburton4296]

Agda code can inter-operate well with Haskell, so it's useful for proving some critical piece of functionality correct (e.g. some cryptographic routine) which is then used by "normal" Haskell code.

[@alkouille2794]

it is definitely not for toy problems

[@Axman6]

There is a vast ocean of programs between “toy programs” and “every day usage”, but Adga can certainly be used for much more real world problems than this intentionally toy example would make you think. See seL4 for an example, the worlds first completely formally verified OS kernel; proven not to terminate unless there is a hardware fault, and should by DARPA’s red teams to be as far as we know to be unhackable, even with root access to a Linux VM running on top of it.

[@XenoTravis]

I was so confused on just the syntax of this language that I could barely follow. What a weird language. I would never want to use this.

[@Prutswerk]

I absolutely agree. It maybe does the job when it comes to eliminating runtime errors but I rather go back to assembly language then using this cryptic looking gibberish.

[@northcode_]

This doesn't really look that different from any ML-like language like Haskell. Obviously any "real" program in this language would use more libraries and convenience functions, he's doing very basic things here and reimplementing standard functionality to show how it works. If you are confused about this go read about lambda calculus and other purely functional languages.

[@eyemotif]

@@northcode_ or f# :D

[@XenoTravis]

@@Prutswerk even assembly is more readable and makes more sense. I wonder who decided to make stuff like _ :: _ but make it space sensitive as well.

[@jakx2ob]

All language is gibberish before you understand the syntax. Perhaps he could have done a better job explaining it but it's really not that bad. Structures like pattern matching are really neat and making their way into more and more mainstream programming languages, but not obvious when you have never worked with them.

[@N0Xa880iUL]

11 seconds

[@nezu_cc]

31

[@N0Xa880iUL]

@@nezu_cc cool!

[@craneology]

Why would you assume your viewers can read Agda without any explanation at all? Bad video.

[@ThorstenAltenkirch]

How do you explain programming if not by example?

[@omgomgomgd]

Looks like haskell, and that pains me greatly. I wish that these kinds of projects would stray less from the familiar C-style syntax that the most productive programmers prefer. Yes I'm throwing shade.

[@computer-love]

are you unwilling to learn something new?

[@omgomgomgd]

@@computer-love No, but everything about such languages rubs me the wrong way. A pretentious, condescending way.

[@Chase-up3do]

Is it truly fair to criticize a language on such a subjective topic? Have we, as programmers, reached the stage where we pretend to be boomers who only say "change terrifies me"? Have humans, in general, ever regretted innovation, no matter how brave? Should I refuse to learn python just because it uses indentation instead of purely semicolons, even though it's quite useful as a scripting language? Should I refuse to learn haskell just because it uses a declarative style syntax with minimal visual clutter, even though it can teach me so much about writing safe, and correct programs even outside of haskell? I don't think we need to be so petty. The point of being a programmer, is to embrace innovation - especially when everything around us is on fire with terrible bugs and horror stories. Perhaps all the research papers written by real computer scientists can teach us something? Perhaps we should pay, at least, some attention to the math behind our hacks?

[@冥-m2q]

@@omgomgomgd Going through the comments in this video I seem to notice more condescending opinions from "productive" or "real-world" programmers than those familiar with functional programming and dependently-typed languages. Though I agree that there's a lot to be done in terms of escaping the ivory tower in both sides.

[@alkouille2794]

C-like syntax would definitely be unreadable in a language like agda. Either way as @Chase said syntax doesn't really matter, it is not what is important

[@markuspfeifer8473]

Naja :D

Now, show us some REAL programs. I want to see ifs, loops, changing state, I/O, etc.

[@chriswarburton4296]

`if` is a form of branching (in fact, the most feeble form there can be, between a 1 or a 0); the video showed more powerful forms branching, including branching on whether a number is zero or non-zero, whether a list is empty or non-empty and whether a finite number is zero or non-zero. Interestingly in the latter example, branching on whether a finite number is zero/non-zero also caused the types of those numbers to branch, between one and greater-than-one, respectively; and this, in turn, caused the vector of that length to branch, such that the case for the empty vector disappeared (since neither of those lengths contains an empty vector). The video also showed loops, via recursion (which is much simpler, and safer and more powerful than looping). The video also showed changing state, represented by recursive calls (see "the state monad", AKA a tuple). Showing infinite loops via co-induction would be cool though :) Agda implements I/O in a similar way to Haskell: individual I/O operations are composed together into larger I/O operations, until eventually we have one big I/O operation which performs everything we want, and to have that execute we give it the name "main".

I appreciate the effort, but know that you're talking to a brain addled imperative programmer. I understood nothing of what you just said.

[@chriswarburton4296]

@ Agda doesn't have statements, so we can't write an equivalent to C's 'if/else', but it does have expressions so we can write an equivalent to C's ternary 'myBool? foo : bar'. Here's an Agda equivalent: data Boolean: Set where True : Boolean False : Boolean This declares a type called Boolean (more specifically it's a Set, meaning it's a type of values, not a type of types); we're declaring that there are two ways to make/construct a Boolean: True is a Boolean and False is a Boolean. We don't actually need to write this ourselves, it's in Agda's standard library. The Agda equivalent to the ternary expression above is a `case` expression, e.g. case myBool of True -> foo False -> bar It's very common to use case expressions on a function's argument, so there's a shorthand for that: myFunction myBoolean = case myBoolean of True -> foo False -> bar Is equivalent to: myFunction True = foo myFunction False = bar Notice that's how functions are being defined in the video, except they're branching on the value of numbers and lists, rather than the value of a boolean. Booleans are actually tedious and unsafe (a phenomenon called "boolean blindness"). For example, here's a C-style program which sums the elements of a list: int sum(List[int] l) { if (isEmpty(l)) { return 0; } else { int x = head(l); int total = sum(tail(l)); return x + total; } } This is incredibly unsafe, since the 'head' and 'tail' functions make no sense if they're given an empty list (e.g. they may crash, throw an exception, etc.). We should only call them on lists which are not empty, which we can check using the isEmpty function. Yet the computer has no way of checking whether we're using these things safely! We could swap the branches around and the program would compile successfully; or we could even remove the isEmpty check entirely! This sort of implicit coupling is a cause of MANY bugs and security vulnerabilities. We can do much better if we stop using Booleans, since they don't give us enough information to check such things. Instead, we can branch directly on the list itself, e.g. in Agda: sum: List Int -> Int sum [] = 0 sum (x :: xs) = x + sum xs Not only is this much clearer and easier to write, there's also no way for us to mix up the branches (the variables 'x' and 'xs' aren't defined in the empty case), and it can't crash (e.g. by trying to take the head of an empty list). This is just normal day-to-day functional programming; where Agda shines is that we can use the type of each branch to narrow-down the types of other parts of the program. For example, the video defines vector lookup like this (I've used the name 'vectorLookup', rather than _!!_ used in the video): vectorLookup: Vec n t -> Fin n -> t vectorLookup (x :: xs) zero = x vectorLookup (x :: xs) (succ n) = vectorLookup xs n This is equivalent to the following case expressions (again, this is like a more powerful form of ternary/switch): vectorLookup v i = case v of x :: xs -> case i of zero -> x succ n -> vectorLookup xs n The reason this is interesting is that when we do 'case v of', there is only one branch. Where is the branch for an empty vector? We could write it, but it will look like this: vectorLookup v i = case v of [] -> case i of () x :: xs -> case i of zero -> x succ n -> vectorLookup xs n This branch '[] -> case i of ()' contains a case expression which doesn't return any value. That's because this case expression is "absurd", i.e. there is no way to ever reach this code. Consider the types: v has type 'Vec n t', and in this branch its value is '[] : Vec 0 t'; hence 'n' must be 0. We're branching on 'i : Fin n', but we know n is 0, so we're branching on 'i: Fin 0'. Which possible values have type 'Fin 0'? There aren't any! If we look at the definition of Fin, it has 'zero : Fin 1' and 'succ : Fin n -> Fin (succ n)', so the smallest FIn type which has any values at all is 'Fin 1'. That's why this is absurd, and Agda can see that we don't need to write that branch. Again, that's much safer, and more convenient, than defining a whole bunch of booleans, juggling them with if-statements and ternaries, and hoping we got things the right way around!

@@chriswarburton4296 Is there a "pure functional programming for imperative programmers" book, or article, or anything that I could read? I understand the overall idea of functional programming (no side effects means fewer bugs), and I employ it in my work whenever I can, but fully replacing flow control statements with whatever this is is gibberish to me.

@@chriswarburton4296 Oh wait, your comment is much longer. brb reading

[@thenorup]

This has to be the worst looking programming language I have ever seen. Anybody know of anything worse?

[@Tomyk9991]

Brainfuck maybe

[@RenX3133]

Its basically Haskell functional language

[@relt_]

@@Tomyk9991 brainfuck is a lot more readable than this

[@solitudesf8111]

apl

[@aether9539]

Javascript

[@MikeCarusoGPlus]

I hope I retire before this becomes a thing.

[@declup]

How do you mean "becomes a thing"? Because agda's been around since about 1999 and is rather popular amongst type theorists and other researchers who work in both math and computer science.

[@Axman6]

“I hope that my industry never progressed” is a pretty lame attitude.

[@astroid-ws4py]

Actually I hope it becomes a thing, Also some blockchain system implementations used those languages to prove that their blockchain protocol works (I have encountered one that uses Coq a few month ago in a job posting), Killing bugs through mathematical proofs is the king level of software engineering.

[@Nors2Ka]

Seems like a nightmare of a language to work with.