forked from alex-eg/sex
implement type inference
Two things out of one mechanism. `_' as a type means "work it out from
the initializer", so (var n _ (strlen s)) stops needing size-t spelled
out; `type-of' hands a macro the type of an expression, so a macro can
dispatch on what it was handed rather than on what was declared. Both
read the same answers from two sides.
Algorithm W's core, intra-procedural, with the extensions C forces:
- an unknown type, since (include stdio.h) brings in names we never
parsed. Unification is consistency rather than equality, so
anything touching an unparsed declaration stops constraining
instead of rejecting a program that compiled yesterday;
- the usual arithmetic conversions, since `+' is not a function of
one type;
- checking mode for initializers, since #(0 0) has no type of its own
and takes one from its context. #(T : ...) is the way out of that.
What it wanted on the way:
- what type a *name* has, which neither the typedef nor the tag
database recorded. One table serves functions and variables, since
a function type already has a surface spelling;
- a scope chain, so a (var c int 9) inside a do ends with the block;
- form-type, keyed by cons cell, so one form has one type;
- macros expanded during the walk rather than before it, so type-of
is answered in the scope the macro was written in.
Closures take the same machinery: a receiver whose type comes from a
call, captures written (name expr) and typed from the expression, and
conversion from a bare function wherever a closure is expected.
type-match grew `_' on the pattern side, since (closure ((int)) int)
and (closure ((float)) int) were separate clauses for one case.
This commit is contained in:
178
tests/sex-programs/inference.sex
Normal file
178
tests/sex-programs/inference.sex
Normal file
@@ -0,0 +1,178 @@
|
||||
(input)
|
||||
(output "15"
|
||||
"42 0.25"
|
||||
"(5, 7)"
|
||||
"(1, 2)"
|
||||
"3"
|
||||
"(5, 7)"
|
||||
"0 1 4 9 "
|
||||
"4"
|
||||
"42"
|
||||
"<closure of 0: 10>"
|
||||
"42"
|
||||
"2 1"
|
||||
"Hello from Sex!")
|
||||
(return 0)
|
||||
|
||||
;;; Both halves of inference, from the two sides that read the same
|
||||
;;; answers: `_' in a type means "work it out", and `type-of' hands a
|
||||
;;; macro the type of an expression.
|
||||
;;;
|
||||
;;; This was written as a draft before either existed, to be read
|
||||
;;; before it was built. It is registered now.
|
||||
;;;
|
||||
;;; Two features, one mechanism:
|
||||
;;;
|
||||
;;; `_' in a type means "work it out", and
|
||||
;;; `type-of' hands a macro the type of an expression.
|
||||
;;;
|
||||
;;; Both are the same solved constraint store, read from two sides.
|
||||
|
||||
(include stdio.h)
|
||||
(include string.h)
|
||||
|
||||
;;; `(include string.h)' is for the C compiler; it tells Sex nothing.
|
||||
;;; A signature has to be written before `_' can be resolved from a
|
||||
;;; call to `strlen' -- without one the call's type is `?', and a `_'
|
||||
;;; that resolves to `?' is an error, not a silent int.
|
||||
(extern fn strlen ((s (* const char))) size-t)
|
||||
|
||||
(struct point ((x int) (y int)))
|
||||
|
||||
(fn midpoint ((a (* const struct point)) (b (* const struct point))) (struct point)
|
||||
(var m (struct point))
|
||||
;; No `_' here: `m' has no initializer to infer from. Inference fills
|
||||
;; in a type, it does not invent one.
|
||||
(= (. m x) (/ (+ (-> a x) (-> b x)) 2))
|
||||
(= (. m y) (/ (+ (-> a y) (-> b y)) 2))
|
||||
(return m))
|
||||
|
||||
;;; The closure's type is written once, in the signature; `_' reads it
|
||||
;;; from there at every use.
|
||||
(fn make-adder ((n int)) (closure ((int)) int)
|
||||
(return (closure ((b int)) int (n)
|
||||
(return (+ n b)))))
|
||||
|
||||
;;; A macro that asks what it was handed.
|
||||
;;;
|
||||
;;; `type-of' returns a *surface* type -- the same spelling the type
|
||||
;;; database hands to `map-fields' -- so it composes with the
|
||||
;;; `type-match' that already exists, and dispatch over a user struct
|
||||
;;; costs nothing extra.
|
||||
(defmacro (print x)
|
||||
(type-match (type-of x)
|
||||
(int `(printf "%d\n" ,x))
|
||||
(size-t `(printf "%zu\n" ,x))
|
||||
(double `(printf "%g\n" ,x))
|
||||
((* const char) `(printf "%s\n" ,x))
|
||||
;; NOTE: ,x twice -- a macro that duplicates its argument still has
|
||||
;; to think about evaluating it twice. Inference does not fix that.
|
||||
((struct point) `(printf "(%d, %d)\n" (. ,x x) (. ,x y)))
|
||||
;; a closure is a type like any other, so it dispatches like one --
|
||||
;; and `_' saves a clause per signature
|
||||
((closure _ int) `(printf "<closure of 0: %d>\n" (,x 0)))
|
||||
(else (error "print: don't know how to print" (type-of x)))))
|
||||
|
||||
;;; The temporary's type is the thing the macro could not write down
|
||||
;;; before. Either spelling works -- `_' is the lazier one, and it is
|
||||
;;; inferred in the expansion's own scope.
|
||||
(defmacro (swap a b)
|
||||
`(do (var tmp _ ,a)
|
||||
(= ,a ,b)
|
||||
(= ,b tmp)))
|
||||
|
||||
(pub fn main () int
|
||||
;; Written out, for contrast with everything below it.
|
||||
(var greeting (* const char) "Hello from Sex!")
|
||||
|
||||
;; size-t, from the signature above -- not int, and not a guess.
|
||||
(var n _ (strlen greeting))
|
||||
(printf "%zu\n" n)
|
||||
|
||||
;; Literals carry a constraint, not a type: the int-ish one defaults
|
||||
;; to int, and the mixed division joins to double the way C does.
|
||||
(var count _ (+ 20 22))
|
||||
(var half _ (/ 1.0 4))
|
||||
(printf "%d %g\n" count half)
|
||||
|
||||
;; An aggregate initializer has no type of its own, so the type flows
|
||||
;; in and has to be written. `(var origin _ #(3 4))' is an error --
|
||||
;; there is nothing to infer from.
|
||||
(var origin (struct point) #(3 4))
|
||||
(var corner (struct point) #(7 10))
|
||||
|
||||
;; A compound literal is the way out of that rule: the `:' is where an
|
||||
;; initializer stops needing a type from its context, so `_' has
|
||||
;; something to read after all.
|
||||
(var centre _ #((struct point) : 5 7))
|
||||
(print centre)
|
||||
|
||||
;; ...and the same designated, which names fields instead of counting
|
||||
;; positions.
|
||||
(var offset _ #((struct point) : .x 1 .y 2))
|
||||
(print offset)
|
||||
|
||||
;; A partial type: "a pointer to something". The something arrives
|
||||
;; from the initializer. This is why the wildcard lives in the type
|
||||
;; grammar rather than beside it -- it composes.
|
||||
(var p (* _) (& origin))
|
||||
|
||||
;; Member access reads the same type database the macros do.
|
||||
(var x _ (-> p x))
|
||||
(printf "%d\n" x)
|
||||
|
||||
;; A call into a function Sex has actually parsed: the return type is
|
||||
;; the whole answer, and `print' then dispatches on it.
|
||||
(var mid _ (midpoint (& origin) (& corner)))
|
||||
(print mid)
|
||||
|
||||
;; The loop variable, which is where `_' earns its keep most often.
|
||||
(for (var i _ 0) (< i 4) (++ i)
|
||||
(printf "%d " (* i i)))
|
||||
(printf "\n")
|
||||
|
||||
;; Four of something: the element type is fixed by the initializer,
|
||||
;; the count by the type. Subscripting gives the element type back.
|
||||
(var squares [_ 4] #(0 1 4 9))
|
||||
(print [squares 2])
|
||||
|
||||
;; A closure's type comes from the signature that produced it, and
|
||||
;; calling one needs that type and nothing else.
|
||||
(var add-10 _ (make-adder 10))
|
||||
(print (add-10 32))
|
||||
(print add-10)
|
||||
|
||||
;; ...including where it is returned, with no name in between.
|
||||
(print ((make-adder 20) 22))
|
||||
|
||||
;; A macro writing a declaration it could not have written before.
|
||||
(var a _ 1)
|
||||
(var b _ 2)
|
||||
(swap a b)
|
||||
(printf "%d %d\n" a b)
|
||||
|
||||
(print greeting)
|
||||
(return 0))
|
||||
|
||||
;;; Open questions this draft raises, to settle before Layer 2 ships:
|
||||
;;;
|
||||
;;; 1. SETTLED. `type-match' took `_' on the pattern side, so
|
||||
;;; `(closure _ int)' above is one clause rather than one per
|
||||
;;; signature, and `(* _)' and `(¤ _ _)' say "any pointer" and "any
|
||||
;;; array". A `_' written last takes the rest, since a type's words
|
||||
;;; are spread and not nested: `(* const char)' is three elements.
|
||||
;;; Nothing destructures -- a macro body is Scheme and a type is a
|
||||
;;; list, so `(caddr (type-of x))' reads an array's length.
|
||||
;;;
|
||||
;;; 2. SETTLED, allowed. `[_ 4]' against `#(0 1 4 9)' unifies each
|
||||
;;; element with the hole, so the element type comes from the
|
||||
;;; literals and the length stays as written -- `[_ 10]' with two
|
||||
;;; initializers is still ten. Elements that disagree are a type
|
||||
;;; mismatch. A bare `_' is still refused: `#(0 1 4 9)' has no type
|
||||
;;; of its own, only elements.
|
||||
;;;
|
||||
;;; 3. POSTPONED to the standard library design. `(extern fn strlen
|
||||
;;; ...)' above duplicates string.h, which is the same bargain every
|
||||
;;; FFI makes, but it is where "no C header parsing" starts costing
|
||||
;;; the user something. A `sex/libc' module of prototypes is the
|
||||
;;; obvious answer and belongs with the rest of the stdlib.
|
||||
Reference in New Issue
Block a user