dependent types in Lisp (Idris BTFO)
Name:
Anonymous
2018-12-17 1:29
;;--------------------------------------------------------------------
;;-- Types
;; slot-number type
(defun within-slot-number-rangep (n)
(not (or (< n 0) (> n 255))))
(deftype slot-number ()
`(and fixnum (satisfies within-slot-number-rangep)))
;; vitality type
(defun within-vitality-rangep (v)
(not (or (< v -1) (> v 65535))))
(deftype vitality ()
`(and fixnum (satisfies within-vitality-rangep)))
;; field type
(deftype field ()
`(or fixnum function))
(deftype field-application ()
`(and function))
;;--------------------------------------------------------------------
;;-- Structures
;; slot structure
(defstruct slot
(number 0 :type index)
(field #'identity :type field)
(vitality 10000 :type vitality))
Name:
Anonymous
2018-12-17 2:32
I don't see any function that takes a value and returns a type. How is this an example of dependent types?
Name:
Anonymous
2018-12-17 8:08
dependent types would have prevented this
Name:
Anonymous
2018-12-18 23:43
>>2did you not see DEFTYPE?
Name:
Anonymous
2018-12-19 5:58
>>4I saw it but I do not think that it defines a function that takes a value and returns a type.
Name:
Anonymous
2018-12-19 17:08
>>5deftype can take parameters and can run arbitrary functions. it returns a type that Common Lisp checks at compile time.
Name:
Anonymous
2018-12-20 4:58
>>5#define type1 int
#define type2 float
#define rettype(num) type##num
Name:
Anonymous
2018-12-20 6:01
>>7Not a function.
>>6How would you represent a list that has its length as part of its type?
Name:
Anonymous
2018-12-20 7:25
>>7#include <dependent-void.h>