Art Theory

Programming with Math (Exploring Type Theory)



Coding Tech

As programs are getting more complex, it’s time to go back to basics, to the old well tested approach to complexity called mathematics. Let compilers deal with the intricacies of Turing machines. Our strength is abstract thinking. Let’s use it!

EVENT:

Øredev 2018

SPEAKER:

Bartosz Milewski

PERMISSIONS:

Conference Organizer provided Coding Tech with the permission to republish this video.

Source

Similar Posts

26 thoughts on “Programming with Math (Exploring Type Theory)
  1. This is amazing! I just love how Bartosz can relate all those subjects and build argumental bridges between them. I'll keep studying as much as I can while I program in JavaScript hehe 🙁

  2. It's funny. The exact reasons that people hate types in programming are exactly the same reasons why many hate types in mathematics.

  3. Simone Should Really try to code in one of the ML languages like F#, sml or so.

    They are some of the most strongly typed languages and I have nearly never had a problem with creating a generic code. But then they are functional which scares people.

    One example are generic filtering mapping, folding and more.

    Seriously think of this scenario.

    You have some collection and want to make some function filter which take some predicate and a instance of that collection it then should return the same type of collection with only those item where the predicate are true.

    In F# this can be done with 4 line of code

    let rec filter pred = function
    | [] -> []
    | x :: xs when pred x -> x :: filter pred xs
    | _ :: xs -> filter pred xs

    This is for most rather strange looking code for those use to C#, java and such. First of all we do not give any clue to the compiler which type to use, it can for around 90% of the time do it without your help. 2 advanced pattern matching (not switch). F# has structural decomposition. Which means we can pattern match structures. The keyword function is to tell that the next to com should be a pattern match over some input not defined. The patterns below tells the compiler which type of argument to expect. Here we are going with lists.
    First pattern er the empty list the arrow means map to right hand side. Her the empty list itself i.e. fixpoint. The second line are the pattern which is a none empty list (x :: xs) where there :: is a pattern construct which separate the head x of the list and the tail xs. When is a guard telling the compiler to only accept when the following expression return true. We here cons the head to the filtered list given by the recursive call to the function. The last case are alle other cases. There is a lot of subtleties to it I haven't given. But the idea should be understand F# has the right type system implemented not.thst adhoc system that are talked about in this video. It fully support imperative, OO, and event driven coding. You don't need delegates to pass functiona as arguments 😆

    This is also very easy to test. There are no mutability so no unit testing. There are two cases, the empty list, some list where some items returns true.

  4. What he is talking about here is very interesting, but it's presented very half-assedly and with very little insight into the real concepts and ideas behind all the symbolic and mathematical jargon he is using… which makes me doubt he really understands what he is talking about.
    If you want to explore type theory in a much more detailed way I suggest giving the "Coq" language a go, it has a nice IDE and some videos on youtube explaining it. Now with that you'll really get to wrestle with the mathematical concepts and it'll at least give you a glimpse into the depth of the theories merely glazed here.
    I have to say I really don't like these types of talks because the viewer/listener often gets very confused and is left with heaps of questions and half-assed half-understood concepts and ideas that are more frustrating (at least to me) than inspiring. I guess it should then spark the viewer to go do their own research by themselves, but realistically they don't do it, and the whole thing was then just a waste of time.

  5. I think the main reason people dislike types is compilation, plain JS does not need any tooling around it – but TS is a different story

  6. generally my vars don’t change type but sometimes i do want to cast between types without expending another var name. imo no big deal either way

  7. There are many things wrong in this talk:
    1. Not everyone hates types, don't generalize.
    2. Generics are not difficult to write; stop bringing up c++ as an example; one language being awkward at generics doesn't mean all of them are.
    3. "Working with types requires learning a new language" — excuse me? don't exaggerate
    4. "Type errors are cryptic". Be specific and say C++ template errors are cryptic. No all langs are like this.
    5. "Types limit our ability to reuse code" … simply wrong. I can create a type(interface) that other objects can implement to make code more reusable.

    There's nothing new here other than fancy terminology, we've been abstracting over types for a long time.

Comments are closed.

WP2Social Auto Publish Powered By : XYZScripts.com