# Re: [stack] Motivations to embrace decidable type systems

## John Nowak — 2009-04-05 06:15:21

    On Apr 4, 2009, at 9:01 PM, hallucious wrote:

     > One motivation for this work was to broaden the range of functions

    > which can be investigated by looking at their type, which can be

    > useful to see their effect.

     You may want to look at Djinn if you haven't already:

    http://lambda-the-ultimate.org/node/1178

     > Another was to allow the programmer to provide additional

    > constraints. I also hoped that the type would form a basis for

    > proving properties of any function, using denotation provided by the

    > programmer.

     In my opinion, it would be more useful to add types dependent on

    values rather than (or in addition to) higher rank polymorphism and

    subtyping if your goal to allow programmers to prove things. There

    are, as you probably know, a large number of languages that already

    take this approach (Agda, Coq, Epigram, Dependent ML, ATS, etc).

     > I do not expect that there is any automated (unguided) procedure to

    > check, for instance, whether two type formulas are equivalent in

    > this system. (Is this what decidable type inference means?)

     In practice, I believe undecidable just means "not guaranteed to

    terminate". For example, type inference is undecidable in a language

    like Agda because certain programs will cause the type checking stage

    to never finish.

    - John