• Liked Abdulsattar Mohammed
    keyboard_arrow_down

    Dependently Typed Programming with Idris

    Abdulsattar Mohammed
    Abdulsattar Mohammed
    schedule 1 year ago
    Sold Out!
    45 mins
    Talk
    Intermediate

    Types allow us to structure data to match the functional requirements of the problem we are trying to solve. But, in most languages, we end up choosing/building types that are the closest to our requirement. They don't exactly fit our bill, as a result of which, we write runtime code to enforce those conditions. Then we write tests because the compiler can't help us. Dependently Typed Languages like Idris allow us to encode a wide range of invariants into the type itself allowing us to possibly have zero runtime errors.

Sorry, no proposals found under this section.