1. 36

  2. 5

    Fantastic introduction to Idris, thanks for sharing. I really liked how you demonstrated the benefits of the language and tooling. The examples were incremental and approachable for someone like me that has never read or written Idris before.

    1. 3

      It kind of mirrors the approach I’ve seen in Edwin Brady’s book Type Driven Development in Idris. Lots of incremental build up, framing dependent types as a ‘natural extension of regular types’ rather than as something weird or difficult.

    2. 4

      Nice article! One thing I found really amusing was the link to “money being dependent on time”, which says the following (bolding mine):

      The AML product language consists of three primary constructions: state models, products, and risk models. Products represent a collection of (condi- tional) payments. Risk models describe the transition intensities. State models simply ensure that products and compatible risk models are used together

      Formal methods only become useful when we figure out how to represent state machines in them.

      (To be clear, this isn’t a problem with either article! It’s just the pattern of “we’ve figured out an awesome way of proving stuff, let’s use it to build state machines” just keeps happening! I take it as a sign we need to study state machines more.)

      1. 1

        You’re right. They’ve just got tons of work done on state machines and functions. Most work on state machines is in hardware and protocol research. They’re almost always FSM’s at some level. Formal verification is common in hardware. The gap is in easily connecting proven, high-level components to low-level, efficient components like FSM’s. Also, functional to imperative. That’s where you see research such as seL4’s Haskell to C combo. I think most work should focus on that, esp with generic transformations.

        An exciting example was Lammich’s Imperative/HOL that certifies conversion of functional, data structures to imperative ones with C++-like performance. CakeML and CompCert themselves are examples. I started collecting lots of stuff on ASM’s and verified metaprogramming/templates since I think that combo has highest, potential payoff. ASM’s are close to FSM’s. The metaprogramming could bring the ASM’s closer to high-level languages.

      2. 3

        One nice trick with dependent types is using them to run unit tests, e.g.

        -- Calculates a type based on a given Bool
        check :: Bool -> Type
        check True  = Unit  -- The "unit type" containing one value, AKA an empty tuple AKA null
        check False = Void  -- The "empty type" containing no values
        -- Some arbitrary unit test, returning either True or False
        testFoo : Bool
        testFoo = foo > bar
        -- The *type* of checkFoo depends on the *value* of testFoo, hence the type-checker
        -- must run the test at compile time
        checkFoo : check testFoo
        checkFoo = null

        Here the value null has type Unit, so checkFoo is only well-typed if its type is Unit. This forces the type checker to run check testFoo, to see whether or not it returns Unit. It will return Unit (and hence pass the type checker) if testFoo returns True (i.e. the test passes).

        If testFoo returns False (i.e. the test fails), then check testFoo will return Void, which means that checkFoo has type Void, which means that null is not a well-typed return value for checkFoo.

        Notice that we don’t have to use Unit and Void, we could use any two distinct types (e.g. Bool and Int). The advantage to using Unit is that we avoid redundancy, since there’s only one possible value to use (null). The advantage to using Void is that there’s nothing we can put as the return value of checkFoo that will work, since Void has no values. (If we picked Bool and Int, we could imagine a lazy developer changing checkFoo to return 42, which would cause the type-checker to succeed despite the testFoo test failing!).

        In fact, the above won’t work in Idris without the following:

        Unit : Type
        Unit = ()
        null : Unit
        null = ()

        This is because, rather confusingly, the unit type in Idris is called () and its (only) value is also called () (i.e. there is a value () : () and there is a type () : Type). I used the unambiguous names Unit and null to avoid ambiguity (although the name null may actually clash with a built-in function :P )