[bitc-dev] Typeclasses and Bitc Logic language

[Swaroop Sridhar]

Since we have a mechanism of expressing dependent type constraints
with type-classes, I think the BitC verification language should
consider exploiting it. I have an example below, which -- in a primitive
form -- shows how we can express and prove some properties similar to twelf.

Hallgren' paper [*] called "Fun with Functional Dependencies" is very 
simple to read, and explains how type-classes and instances can be used 
to statically model computation and "execute" it.

[*] T. Hallgren. Fun with functional dependencies. In Joint Winter 
Meeting of the Departments of Science and Computer Engineering, Chalmers 
University of Technology and Goteborg University, Varberg, Sweden, Jan. 
2001.
http://www.cs.chalmers.se/~hallgren/Papers/wm01.html

________________________________________________________________________

(defstruct none)
(defstruct (some 'a 'b))
(defstruct (readable 'a))
(defstruct (writable 'a))

(deftypeclass (Create 'a 'b 'c)
	       (tyfn ('a, 'b) ~> 'c)
	create: (fn ('a 'b) 'c))

(definstance (create none 'a (some 'a none))
(definstance (create 'a 'b 'c) => (create 'c 'd (some 'c 'd))

(deftypeclass (Xfer 'a 'b 'c 'd)
	(tyfn ('a 'b 'c) ~> 'd)
	xfer: (fn ('a 'b 'c) 'd)
  )

(definstance (Xfer (readable 'a) 'b (some 'b 'd)
					(some (readable 'b) 'd))

(definstance (Xfer (readable 'a) 'b (some (readable 'b) 'd)
					(some (readable 'b) 'd))
(definstance (Xfer 'a 'b 'c) => (Xfer 'a 'b (some 'd 'c)))

(deftype myCap #x1) ; dymmy type, I am using deftype for better
                     ;documentation.
(deftype yourCap #x2)

(define a:(readable myCap) _)
(define b:yourCap _)
(define empty:none)

(define newList (create a none))
;; newList: (some (readable myCap) none)

(define newerList (create b newList)) 	
;; newerList: (some yourCap (some (readable myCap) none))

(define brandNewList (Xfer a b newerList))
;; brandNewList: (some (readable yourCap) (some (readable myCap) none))

(deftypeclass (IsWritable 'a 'b))
(instance (IsWritable 'a (some (writable 'a) 'b))
(instance (IsWritable 'a 'b) => (IsWritable 'a (some 'c 'b)))

;; Similarly for IsReadable

(define findOutReadable: (isReadable yourCap brandNewList))
;; OK, well typed

(define findOutWritable: (isWritable yourCap brandNewList))
;; FAILED no such instance