type-rep.shen

(define string-concat
{ (list string) --> string }
  [] -> ""
  [S] -> S
  [S | Ss] -> (@s S " " (string-concat Ss)))

(datatype verified-types-for-lists

  _______________________________________
  (empty? Xs) : verified >> Xs : (list A);

  _______________________________________
  (cons? Xs) : verified >> Xs : (list A);)

(define ->str
{ A --> string }
  Xs -> "()" where (empty? Xs)
  Xs -> (@s "(" (string-concat (map ->str Xs)) ")") where (cons? Xs)
  Str -> (str Str))

(datatype type-reps

  _____________________________________________
  X : (type-rep A) >> (get X type-rep) : string;


  let Tag (put (eval X) type-rep (->str A))
  (tag-value-with-rep X A);
  X : A; (tag-value-with-rep X A);
  __________________________________________
  X : (type-rep A);)

(define type-of
  { (type-rep A) --> string }
  X -> (get X type-rep))