Proxy, Typeable, and TypeReps

[aijony]

Facilitates the introspection of types.

• (typeOf 1) => Integer
• (typeRep (the (Proxy (Arrow Integer)) Proxy) => (-> Integer)

Every defined type is Typeable.

Depends on: #681

[gefjon]

Can typeRep, toProxy and typeOf be type-rep, to-proxy and type-of, please?

[eliaslfox]

I think it might be possible to do Typeable without poly kinds.

The api would be the same:

(define-type TypeRep)

(define-class (Typeable :a)
  (typeOf (Typeable :a => :a -> TypeRep)))

But the compiler generated instances would look a little different:

(define-type Unit)

(define-instance (Typeable Unit)) ;; compiler written

(define-type (Proxy :a) Proxy)

(define-instance (Typeable :a => Typeable (Proxy :a))) ;; compiler written

The instances without constraints are trivial:

(define-global-lexical |INSTANCE/TYPEABLE UNIT| coalton-impl/typechecker::*unit-type*)

Instances with constraints will need a little codegen magic:

(defun |INSTANCE/TYPEABLE PROXY :A| (#G403) 
  (coalton-impl/typechecker::%make-tapp
    coalton-library/typeable::*proxy-type* ;; not actually a special variable, needs to be pulled from env
    #G403)) ;; access secret parameter

[eliaslfox]

Closing as this would have required #681.