Possible topic for focused study and discussion

[Matt Oliveri]

Since no one has come forward with an idea for a specific goal for the study group, I decided to propose one and see if there's interest.

There are at least four distinct "flavors" of system related to dependent type theory:

1. "Truly" dependent type systems
2. Type systems for programming languages that imitate dependent typing to various degrees
3. Program logics
4. Predicate logics with type systems

(Of course these three categories are still broad.)
Examples of systems in the categories:
1. Martin-Löf Type Theory, Computational Type Theory, Edinburgh LF, Calculus of Constructions, HoTT, Cayenne, Zombie, F*
2. ATS, Habit, Scala (path-dependent types), "Hasochism"
3. Hoare logic, LCF, ACL2, Spec#, Computational Type Theory (again)
4. Many-sorted first-order logic, Curch's HOL, FOLDS

Talking to other programming language enthusiasts, and reading discussion threads on Lambda the Ultimate, I've gotten the impression that many programmers are not that clear on the differences between these things. What seems well-known is that type systems are connected to mathematical logic by the Curry-Howard correspondence, and dependent type systems are a particularly rich style of system related to this, and they also let you reason about programs. But a detailed appreciation of what sets truly dependent type systems apart seems missing from many programming-oriented discussions of dependent types.

I am particularly interested in discussing, once the prerequisites are understood, what the possible advantages of true dependency are, for programming and/or for math. It cannot just be assumed that there's real benefit to it! A skeptic could point out that programmers and mathematicians have traditionally got along fine without knowing about dependent types; maybe they're not so great. Should that attitude be challenged? How?

[Matt Oliveri]

On Friday, May 13, 2016 at 7:30:40 PM UTC-4, Matt Oliveri wrote:

Since no one has come forward with an idea for a specific goal for the study group, I decided to propose one and see if there's interest.

There are at least four distinct "flavors" of system related to dependent type theory:

1. "Truly" dependent type systems
2. Type systems for programming languages that imitate dependent typing to various degrees
3. Program logics
4. Predicate logics with type systems

(Of course these three categories are still broad.)

Oops. "these four", of course.

[Gavin Mendel-Gleason]

I'd be very keen on discussing these 4 - and indeed what would constitute a sufficient basis of prerequisites for understanding the differences between them. 

*Warning: random opining follows*

"Real world" programming is currently a long way from the use of dependent types, and as someone who has spent a fair bit of time programming in industry, I view this as a bad thing.  So many problems that I encountered could have been solved once and for all by types (SQL injection attacks spring to mind, but also a host of other safety issues)  However, there are good reasons for not employing languages of dependent types, and that's that the costs (largely in human labour) of using them are simply too high at present.  I'd like to see type theory tools deployed in such a way that this is no longer the case.

While I'm interested in the mathematical foundations, and I think it's often the case that mathematical elegance has its own utility even in practice, I lean more towards the programming praxis angle.

I'd be curious to see where dependent types have been deployed in practice already, but also imagining how they might be feasibly deployed and what sort of tool-chain would be necessary to make this a reality.

One thing that particularly impressed me of late was F-star. While It's a bit irritating that you don't get to interact with the theorem prover directly and have to attempt to coax it in the right direction, it does have a lot of the things that I think will prove essential for broadening the appeal and deployment.  For instance, a graded hierarchy from quick and dirty imperative, right up to pure functional -  and all made visible in the type system.  

And while I'm in the rhythm of ranting, I'll go ahead and wager that the following features will prove important:

1. You can start with something akin to one of these modern lisp like languages (garbage collected, dynamically typed but with effects, ala python / javascript) or perhaps something of the ML family (garbage collected, statically typed but with effects ala F#) and "turn up" the type checking for regions of the code that you want to lock down, right up to the point that you have a full dependent type system at your disposal. 

I think this will turn out to be important because: A) for significant amounts of code, the specification is not actually known yet and will only be found as it is explored, B) the code changes too fast for a very careful typing discipline to be desirable and C) because sometimes correctness just matters less than getting the damn thing limping.

Maybe we really can just go full fledged with "pure" functional programs but I'm a bit skeptical that using monad transformers should be necessary to add a debugging print statement when using exceptions. If it goes this route I think it's going to have to force the user to pay less for the price of admission. Perhaps this can be done with suitably cool approaches at the type level.

2. That you have facilities for automating the boring parts of the proof (at the very least). 

I just spent some wicked stupid amount of time doing an obviously banal and decidable proof in Agda by hand - I started using reflection and writing a prover and gave up proving the prover produced the appropriate type after wasting 4 hours when the program to write the program started exceeding the size and time of the boring proof. This should have been 10 minutes max playing with some tactic language.

3. Proof of concept. [not really a feature... but]

The system should be developed with a view to early deployment.  This can help to hone the theoretical approach under the stress of practice.  It's often very hard to choose from among a number of potentially beautiful approaches without the guide of necessity.  My guess is that these problems should be where the cost of disaster is higher than the cost of programmer time. I work with databases a lot and their implementation, and query optimisers etc. are all things which might be amenable to a more formal approach. 

[Hendrik Boom]

On Thu, Jul 14, 2016 at 01:27:25AM -0700, Gavin Mendel-Gleason wrote:
>
> I'd be very keen on discussing these 4 - and indeed what would constitute a
> sufficient basis of prerequisites for understanding the differences between
> them.
>
> *Warning: random opining follows*
>
> "Real world" programming is currently a long way from the use of dependent
> types, and as someone who has spent a fair bit of time programming in
> industry, I view this as a bad thing. So many problems that I encountered
> could have been solved once and for all by types (SQL injection attacks
> spring to mind, but also a host of other safety issues) However, there are
> good reasons for not employing languages of dependent types, and that's
> that the costs (largely in human labour) of using them are simply too high
> at present. I'd like to see type theory tools deployed in such a way that
> this is no longer the case.

I was tinkering with this stuff in the 80's and got so far as proving
a merge sort ws correct, but the machine resources available to me
were insufficient to continue the work.

>
> While I'm interested in the mathematical foundations, and I think it's
> often the case that mathematical elegance has its own utility even in
> practice, I lean more towards the programming praxis angle.

I agree.

> I'd be curious to see where dependent types have been deployed in practice
> already, but also imagining how they might be feasibly deployed and what
> sort of tool-chain would be necessary to make this a reality.
>
> One thing that particularly impressed me of late was F-star. While It's a
> bit irritating that you don't get to interact with the theorem prover
> directly and have to attempt to coax it in the right direction, it does
> have a lot of the things that I think will prove essential for broadening
> the appeal and deployment. For instance, a graded hierarchy from quick and
> dirty imperative, right up to pure functional - and all made visible in
> the type system.

My system was purely functional, based on the Martin-Lof type theory,
The syntax vaguely resembled that of a progrmming language, with
let-clauses, lots of explicit type specifications attached to
expressions using colons, and so forth. I delineratesly did not try
to do anything like a Milner-Hindley type inference system because
dealing with type dependencies was already trouble enough.

the really hard part was determining whether two types were equa, so
that a value of one type could be used as value of another (equal)
type. That, of course is unsolvable, so I had nechanisms whereby the
programmer could guide the proof.

> And while I'm in the rhythm of ranting, I'll go ahead and wager that the
> following features will prove important:
>
> 1. You can start with something akin to one of these modern lisp like
> languages (garbage collected, dynamically typed but with effects, ala
> python / javascript) or perhaps something of the ML family (garbage
> collected, statically typed but with effects ala F#) and "turn up" the type
> checking for regions of the code that you want to lock down, right up to
> the point that you have a full dependent type system at your disposal.

Have a look at typed racket. It's an implementation of a Scheme
dialect with a strong typing discipline optionally imposed on it. The
mechanisms used to securely interface the type-checked code with the
unchecked code is particularly interesting.

Unfortunately, typed Scheme does not do dependent types.

>
> I think this will turn out to be important because: A) for significant
> amounts of code, the specification is not actually known yet and will only
> be found as it is explored, B) the code changes too fast for a very careful
> typing discipline to be desirable and C) because sometimes correctness just
> matters less than getting the damn thing limping.

This is exactly correct. You want full formal verification only where
you need it enough to be able to afford it.

>
> Maybe we really can just go full fledged with "pure" functional programs
> but I'm a bit skeptical that using monad transformers should be necessary
> to add a debugging print statement when using exceptions. If it goes this
> route I think it's going to have to force the user to pay less for the
> price of admission. Perhaps this can be done with suitably cool approaches
> at the type level.
>
> 2. That you have facilities for automating the boring parts of the proof
> (at the very least).

I had some of that for equalilty proving, but not enough. For most
type checking I used a context-dependent type propagation mechanism
similaar to that of Algol 68.

>
> I just spent some wicked stupid amount of time doing an obviously banal and
> decidable proof in Agda by hand - I started using reflection and writing a
> prover and gave up proving the prover produced the appropriate type after
> wasting 4 hours when the program to write the program started exceeding the
> size and time of the boring proof. This should have been 10 minutes max
> playing with some tactic language.

Nothing in my system was interactive. There was no tactic language.

>
> 3. Proof of concept. [not really a feature... but]
>
> The system should be developed with a view to early deployment. This can
> help to hone the theoretical approach under the stress of practice. It's
> often very hard to choose from among a number of potentially beautiful
> approaches without the guide of necessity. My guess is that these problems
> should be where the cost of disaster is higher than the cost of programmer
> time. I work with databases a lot and their implementation, and query
> optimisers etc. are all things which might be amenable to a more formal
> approach.

Exactly.

-- hendrik

[Steven Shaw]

I don't think we should imagine that you can't use a dependently-typed programming language for _all_ your programming needs! You don't always need fancy types or verification. This agrees with Gavin's recent experience with F*. I'm assuming that you can pretty much write F# programs in F*. I'm having a similar experience with Idris. I've ported a couple of simple OCaml programs to Idris just using the "ML subset". It was a fairly straightforward exercises (excepting poor compiler error messages and lack of libraries/tools).

What I find wonderful about languages like Idris (and even Haskell). You can write simple, type-safe programs most of the time and level-up to interesting type system features whenever you hit a problem that might require it. What's more is that you're always exposed to learning opportunities — every day can be a chance to "level up". Also, the fancy types in Idris don't seem nearly as challenging as fancy types in Haskell.

The main problem for industrial use is that none of the dependently-typed programming languages are ready (they're just research prototypes). I hope Idris gets there. In the Microsoft sphere, I also have hopes for F*. Right now, there is some industrial use of Haskell and it's possible that GHC will get full dependent types some time around the corner (though I don't think it'd be possible to use Haskell for verified programming due to it's nature as an inconsistent logic, please correct me). Not sure if it's a race but I reckon industry adoption (similar to the level of Haskell at least) is only 5-10 years off.

Cheers,

Steve.

[Hendrik Boom]

On Fri, Jul 15, 2016 at 02:57:09PM +1000, Steven Shaw wrote:

>
> The main problem for industrial use is that none of the dependently-typed
> programming languages are ready (they're just research prototypes). I hope
> Idris gets there. In the Microsoft sphere, I also have hopes for F*. Right
> now, there is some industrial use of Haskell and it's possible that GHC
> will get full dependent types some time around the corner (though I don't
> think it'd be possible to use Haskell for verified programming due to it's
> nature as an inconsistent logic, please correct me).

If you can code the Y combinattor, the logic is inconsistent by Curry's
paradox. Consider Y not. It's true iff it's false.

You need a machanism to distinguish the termination types and the
descriptive types. One mechanism I've seen:
T: Expressions of type T will terminate and yield a value of type T.
*T: the type of expressions which, if their evaluationn should ever
terminate, will yield a value of type T.

Note: these types aren't disjoint.

Then Y applied to a function f from T to T will yield a function from T
to *T.

-- hendrik

[Matt Oliveri]

Whoa, I missed these messages from ~2 months after my original post.
Now I reply ~1/2 month late. :\

On Thursday, July 14, 2016 at 4:27:25 AM UTC-4, Gavin Mendel-Gleason wrote:

I'd be very keen on discussing these 4 - and indeed what would constitute a sufficient basis of prerequisites for understanding the differences between them.

I think a good first step for someone who has used advanced typed programming languages would be to learn pure type systems (PTS), and how F_omega, intuitionistic HOL, and the Calculus of Constructions (CoC) are represented as PTSs. It's instructive to see how both IHOL and CoC essentially extend F_omega by adding predicates, but in very different ways. CoC is dependently typed, while IHOL is a predicate logic. CoC uses propsitions-as-types, IHOL doesn't. (IHOL propositions are F_omega types, but it thinks of F_omega's kinds as the main types.) Haskell's type system is actually more like IHOL, from what I've heard: predicates apply to "lifted values" which are elements of kinds. The proof theory perspective of this would be that the lifted values are the mathematical objects, and the programs are proofs about them. (In an inconsistent logic.)

Let me know if you'd like a more detailed pointer, or want to discuss it before/after.

*Warning: random opining follows*

"Real world" programming is currently a long way from the use of dependent types, and as someone who has spent a fair bit of time programming in industry, I view this as a bad thing.  So many problems that I encountered could have been solved once and for all by types (SQL injection attacks spring to mind, but also a host of other safety issues)  However, there are good reasons for not employing languages of dependent types, and that's that the costs (largely in human labour) of using them are simply too high at present.  I'd like to see type theory tools deployed in such a way that this is no longer the case.

While I'm interested in the mathematical foundations, and I think it's often the case that mathematical elegance has its own utility even in practice, I lean more towards the programming praxis angle.

I'd be curious to see where dependent types have been deployed in practice already, but also imagining how they might be feasibly deployed and what sort of tool-chain would be necessary to make this a reality.

One thing that particularly impressed me of late was F-star. While It's a bit irritating that you don't get to interact with the theorem prover directly and have to attempt to coax it in the right direction, it does have a lot of the things that I think will prove essential for broadening the appeal and deployment.  For instance, a graded hierarchy from quick and dirty imperative, right up to pure functional -  and all made visible in the type system.

I also think F* is very interesting. I don't trust it though. It's doing something which is semantically pretty subtle, and it doesn't seem like they've done a formal semantic model. Something vaguely like F* will be great someday, but F* itself feels a bit rushed. I agree that their style of automation seems useful, but they should support real interactive proving as well.

And while I'm in the rhythm of ranting, I'll go ahead and wager that the following features will prove important:

1. You can start with something akin to one of these modern lisp like languages (garbage collected, dynamically typed but with effects, ala python / javascript) or perhaps something of the ML family (garbage collected, statically typed but with effects ala F#) and "turn up" the type checking for regions of the code that you want to lock down, right up to the point that you have a full dependent type system at your disposal. 

I think this will turn out to be important because: A) for significant amounts of code, the specification is not actually known yet and will only be found as it is explored, B) the code changes too fast for a very careful typing discipline to be desirable and C) because sometimes correctness just matters less than getting the damn thing limping.

Maybe we really can just go full fledged with "pure" functional programs but I'm a bit skeptical that using monad transformers should be necessary to add a debugging print statement when using exceptions. If it goes this route I think it's going to have to force the user to pay less for the price of admission. Perhaps this can be done with suitably cool approaches at the type level.

I agree that good support for "pay for what you use" is important. I'd like to take this opportunity to praise Computational Type Theory, and bash intrinsically dependent type theories, including Idris.

The way of thinking about intrinsic typing is that types are introduced as abstract collections of objects, and intro and elim operations provide the abstract interface to to these collections. An element of such a type is an object which can only be understood abstractly, via the operations on its (unique) type.

With extrinsic, a.k.a. refinement types, you start with an existing system of objects. They may have interesting intrinsic types, or they may all have one big catch-all intrinsic type. (The latter is an untyped, a.k.a. uni-typed system.) You then organize the objects into collections defined by concrete properties and relations on objects.

Computational type theory is based on refinement types defined in terms of the computational behavior of programs. This sort of type theory naturally provides dependent type constructors in roughly the same way that set theory does. You can assign as many refinement types as you want to an existing program, because the meaning of this is just to prove more and more behavioral properties of the program.

Intrinsic dependent type systems start with a system of types that include--by force--dependent type constructors. Elements of these types can be intuitively thought of as programs, but it seems a stretch of the imagination (to me) that programs could be intrinsically dependently typed. At any rate, two programs, one using only simple type constructions in its type, the other using dependent types, are a priori incomparable. Even if it intuitively seems like they are the same program, but with one having a stronger type, this is an illusion. It makes no sense to ask whether objects with different types are the same. The practical consequence is that to use an intrinsically dependently typed object in a simply typed program, you need to coerce it to a weaker type. Even if the point of the dependent type was intuitively just to prove some fact about the program!

This coercion business can get really bad. Think of the "Fin n" types. Intuitively, (Fin n) is the collection of natural numbers less than n. So intuitively (Fin n) should be a subtype of (Fin (n+1)). Intrinsic typing provides no basis whatsoever for this intuition! In contrast, the refinement version of "Fin n" says exactly that (Fin n) is the subset of those natural numbers m where (m < n). An element of (Fin n) is already an element of (Fin (n+1)). You do not "prove" this by implementing a coercion, you can prove it simply because it's true. Computationally, all Fin elements are just natural numbers. You don't coerce.

In a naive implementation of intrinsic Fin types, coercions from a Fin to Nat, or between Fins need to "reconstruct" the element at a different type. You pay a runtime cost to capture properties that, intuitively, your program already has! Unacceptable! Using intrinsic type systems to try and capture program properties is broken. It's fundamentally flawed. Intrinsic typing is not about properties, it's about abstract structure. Program properties are simply not a matter of intrinsic typing. Quite the contrary: you need to have an intrinsic type in mind to even know which properties apply. Type constructors like Fin and Vec (lists of a given length) are useful, but intrinsic dependent type systems are simply doing them wrong. Intuitively, and in computational type theory, they are refinements of Nat and List which guarantee an additional property. With intrinsic typing, they are families of abstract collections with no a priori relation to Nat and List.

Perhaps somewhere in the wide world of abstract mathematics, there is a place for intrinsic dependent typing. But I don't know of any programming applications.

Interestingly, although intrinsic and refinement dependent typing are fundamentally different, their syntax can be made fairly similar. I conjecture that all the program development techniques that people are trying based on intrinsic typing can be adapted to work at least as well for refinement typing.

Getting back to "pay for what you use", intrinsic dependent typing makes you pay too much, because when you "strengthen" the type of a program, you're actually making an interface-breaking change. Of course this is just nuts. You just wanted to prove a property; it shouldn't change the program at all.