[Prev][Next][Index][Thread]

State of the art in dependent typing?

 > 1. In propositional logic, one can use {x:Nat|x<10} to express the
 > subset of natural numbers less than 10.  Hindley-Milner extensions
 > have been proposed to support subset types, such as Sokolowski's:
 > 
 > 	http://www.ipipan.gda.pl/~stefan/Papers/research.html
 > 
 > This seems very useful; is there a good reason why this hasn't been
 > adopted by languages like Haskell and ML?

One problem is that type inference easily becomes undecidable or
leaves the programmer to prove theorems. 

 > 2. In languages like Augustsson's Cayenne:
 > 
 > 	http://www.cs.chalmers.se/~augustss/cayenne/
 > 
 > One can model both programs and proofs in a uniform language.  Why
 > isn't this an area of huge interest, i.e. with would-be Sun
 > Microsystems trying to popularize new mainstream languages based on
 > this technology?
 > 
 > While Java is receiving tremendous hype, it's mostly an incremental
 > improvement over C++, whereas this stuff is *revolutionary*, having
 > the potential to make commercial software far more reliable.  It seems
 > surprising there isn't widespread interest.

Maybe it is not as bad as you think: recent work by
Pfenning,Harper,Lee,Xi,.. show that you can use dependent types to
make mobile code safer. E.g. Harper & Xi introduced DTAL (Dependently
Typed Assembly Language) and showed how this can be used to safely
avoid array bound checking e.g. in for Java Applets.

 > Is it that people are turned off by the theoretical undecidability of
 > powerful dependent type systems?  This doesn't seem too likely to
 > cause real-world problems -- reasonable programs tend to be easy for a
 > typechecker to analyze.

It depends, e.g. you can use dependent types to express the spec of
your program than programming becomes as hard as proving partial
correctness. Still I think you are right, but the tools are not
yet there. 

 > 3. Is there anything preventing the programs-with-proofs concept from
 > being taken to the extreme?  For example, building abstract
 > definitions of:
 > 
 >     - sets
 >     - monads
 >     - groups
 >     - lambda calculi
 >     - categories
 >     - sorting functions
 > 
 > and concrete instances containing proofs that they obey the
 > appropriate laws.  I've seen a few assorted systems along these lines,
 > but nothing universal.  Has anyone attempted to build a comprehensive
 > set of types and proofs for mathematical objects or categories this
 > way?

I am not sure what it is what you are looking for. Maybe something
like a type-theoretic version of Bourbaki? People have been discussing
the "mathematical vernacular" in Type Theory, but your are right
nothing like this does exist, yet. Although, there are certainly
comprehensive libraries for Systems like COQ or LEGO..

One problem is that TT & its tools are still developing. Another is
that there are different flavours of TT. Per Martin-Löf did not only
introduce dependent types but also a (predicative) philosophy in an
attempt to provide a firm base for mathematical reasoning.

 > 4. I noticed the following analogy between ordinary
 > types and dependent types:
 > 
 >     A=>B <-> All(x:A).B
 >     A*B  <-> Exists(x:A).B
 >     A+B  <-> ___________
 > 
 > Can we fill in the blank meaningfully, i.e. is there a useful notion
 > of "dependent sum"?

No, it doesn't exist. Btw, there is another relation

    AxB	       All(x:A)B or Pi(x:A)B
    A+B        Exists(X:A)B or 

where the left is the "infinitary" version of the right. Now function
spaces is missing...

 > Would it be valid to say that "A+B" is not actually a primitive type
 > itself, but instead corresponds to the existential subset type:
 > 
 >    Exists( {t|t==A or t==B)} ).t

I suupse from a proposition as types point of view there isn't much
gained by reducing "+" to "or". You can certainly use bool to
represent "+"

	  A+B = Exists x:Bool.if x then A else B

To od this you need a "microscopic universe" bool containing
True,False. 

I personally don't think there is any reduction possible here.  Even
in propositional logic you have /\,\/,-> or +,x,-> and hence in TT
+,Sigma,Pi,...

 > 
 > Where the {x|P(x)} represents the notion of "subset types" as
 > described above?  One can read this as: there exists a type t, equal
 > to either A or B, such that we encode a single value of type t.  This
 > encoding of sums is (I think) a more flexible version of Cardelli's
 > "Any/TypeOf/ValueOf" definitions:
 > 
 > 	http://research.microsoft.com/Users/luca/Papers/TypeType.ps
 > 
 > 5. Cayenne has a construct for defining records:
 > 
 >     s = struct {a=1; s="hello";}
 > 
 > Has anyone tried defining such records as functions from strings
 > (corresponding to tags) to dependent types? i.e.:
 > 
 >     s :: (x::String).
 >         if      x="A" then Int;
 >         else if x="s" then String; -- else _|_
 > 
 >     s = \(x:String)->
 >         if      x="A" then 1;
 >         else if x="s" then "hello";
 > 
 > Such functions seem to obey the ordinary rules of records.

I suppose you are exploiting the iso

  AxB ~ Pi x:Bool.if x then A else B

related to the one I mentioned above. However, it is not clear how
to do this for "dependent records" which correspond to generalized
Sigma-Types. I believe that Jason Hickey suggested "very dependent
types" in this context. 

 > A variation on this theme is to represent certain records as
 > "functions from types to dependent types".  These seem to be
 > signature-free records, which may be useful for composing
 > Cayenne-style proofs without committing to specific proof names.
 > 
 > 6. Looking at the bigger picture, are "programs with proofs" of
 > practical value in future commercial software?  I have to wonder if
 > we're simply trading "bugs in programs" for "bugs in proof types".
 > 
 > For example, I can easily write a "qsort" function, test it with
 > sample data, and be pretty confident it's ok.
 > 
 > But, what is the "proof type which all sorting functions must
 > inhabit"?  I have no idea, but suspect it's very complex and dependent
 > on other proofs such as those governing ordering relationships.

Its not so complicated, e.g. have a look at my (now quite dated)
lecture notes: 

http://www.tcs.informatik.uni-muenchen.de/~alti/abstracts.html#ESSLLI96.abstract	

  Given
 > human fallability, it seems just as likely to write the wrong "proof
 > type" (hence prove the wrong thing) as write an buggy program.  Is
 > this a problem in practice?

Sure. There is no perfection but formally checked programs could
provide an essential increase in reliability. Also you could make the
spec part of the contract. Then it is the employers problem (and
economic interest) to provide the correct spec.

Are you sure you are a typical games programmer? :-)

Cheers,
Thorsten

-- 
Dr. Thorsten Altenkirch			phone : (+49 89) 2178-2209
Theoretical Computer Science		fax   : (+49 89) 2178-2238
LMU, D-80538 Munich, Germany		Oettingenstr 67, room D105
http://www.tcs.informatik.uni-muenchen.de/~alti