Skip to content

Commit

Permalink
Merge branch 'main' into type-alias
Browse files Browse the repository at this point in the history
  • Loading branch information
Yarin Heffes authored Oct 16, 2024
2 parents fde68b5 + 7fd033d commit c9ba647
Show file tree
Hide file tree
Showing 27 changed files with 365 additions and 256 deletions.
4 changes: 3 additions & 1 deletion coalton.asd
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,8 @@
(:file "complex")
(:file "elementary")
(:file "dyadic")
(:file "dual")))
(:file "dual")
(:file "package")))
(:file "randomaccess")
(:file "cell")
(:file "tuple")
Expand Down Expand Up @@ -257,6 +258,7 @@
(:file "struct-tests")
(:file "alias-tests")
(:file "list-tests")
(:file "lisparray-tests")
(:file "red-black-tests")
(:file "seq-tests")
(:file "pattern-matching-tests")
Expand Down
20 changes: 10 additions & 10 deletions docs/coalton-lisp-interop.md
Original file line number Diff line number Diff line change
Expand Up @@ -196,28 +196,28 @@ There are two ways to call Coalton from Lisp.
The safe way to call Coalton is to use the `coalton` operator. This will type check, compile, and evaluate a Coalton expression and return its value to Lisp. Note that `coalton` does not accept definitions or top-level forms. For example:

```lisp
CL-USER> (format t "~R" (coalton:coalton coalton-library::(length (cons 1 (cons 2 nil)))))
CL-USER> (format t "~R" (coalton:coalton (coalton-prelude:length (coalton:cons 1 (coalton:cons 2 coalton:nil)))))
two ; <- printed output
NIL ; <- returned value
CL-USER> (format t "~R" (coalton:coalton coalton-library::(length 1)))
CL-USER> (format t "~R" (coalton:coalton (coalton-prelude:length (coalton:the coalton:UFix 1))))
; (Guaranteed Compile-Time Error:)
;
; Failed to unify types COALTON:INTEGER
; and (COALTON-LIBRARY:LIST :B)
; in unification of types (COALTON:INTEGER → :A)
; and ((COALTON-LIBRARY:LIST :B) → COALTON:INTEGER)
; in COALTON
; error: Type mismatch
; --> repl input:1:46
; |
; 1 | (COALTON:COALTON (COALTON-LIBRARY/LIST:LENGTH (COALTON:THE COALTON:UFIX 1)))
; | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Expected type '(COALTON:LIST #T53400)' but got 'COALTON:UFIX'
; [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]
```

### Unsafe Calls

Using the aforementioned promises, it's possible to call into raw Coalton-compiled code by using the generated functions. These calls are not checked in any way!

```lisp
CL-USER> (format t "~R" coalton-library::(length (cons 1 (cons 2 nil))))
CL-USER> (format t "~R" (coalton-prelude:length (coalton:cons 1 (coalton:cons 2 coalton:nil))))
two ; <- printed output
NIL ; <- returned value
CL-USER> (format t "~R" coalton-library::(length 1))
CL-USER> (format t "~R" (coalton-prelude:length 1))
; (Possible Run-Time Error #1:)
;
; The value
Expand Down
52 changes: 30 additions & 22 deletions docs/intro-to-coalton.md
Original file line number Diff line number Diff line change
Expand Up @@ -526,16 +526,14 @@ COALTON-USER> (type-of '/)
∀ :A :B. DIVIDABLE :A :B ⇒ (:A → :A → :B)
```

Because of the generic nature of division, if you're computing some values at the REPL, "raw division" simply does not work.
Because of [Instance Defaulting](#instance-defaulting), division of `Integer` constants without any additional context defaults to `Double-Float` division:

```
COALTON-USER> (coalton (/ 1 2))
Failed to reduce context for DIVIDABLE INTEGER :A
in COALTON
[Condition of type COALTON-IMPL/TYPECHECKER::COALTON-TYPE-ERROR-CONTEXT]
0.5d0
```

You have to constrain the result type of the `Dividable` instance. You can do this with the `the` operator. There are lots of `Dividable` instances made for you.
We can inform Coalton that our constants are of another type by constraining them with `the` or relying on type inference. For example, in order to get a non-Double-Float result from `Integer` inputs, you have to constrain the result type to your desired type (as long as the type has a defined instance of the `Dividable` type class):

```
COALTON-USER> (coalton (the Single-Float (/ 4 2)))
Expand All @@ -544,13 +542,17 @@ COALTON-USER> (coalton (the Fraction (/ 4 2)))
#.(COALTON-LIBRARY::%FRACTION 2 1)
```

But division of integers does not work.
An `Integer` result from division with `/` is not possible, as the instance `Dividable Integer Integer` is not defined:

```
COALTON-USER> (coalton (the Integer (/ 4 2)))
Failed to reduce context for DIVIDABLE INTEGER :A
in COALTON
[Condition of type COALTON-IMPL/TYPECHECKER::COALTON-TYPE-ERROR-CONTEXT]
; error: Unable to codegen
; --> repl input:1:22
; |
; 1 | (COALTON (THE INTEGER (/ 4 2)))
; | ^^^^^^^ expression has type ∀. (RECIPROCABLE INTEGER) => INTEGER with unresolved constraint (RECIPROCABLE INTEGER)
; | ------- Add a type assertion with THE to resolve ambiguity
; [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]
```

Why shouldn't this just be `2`?! The unfortunate answer is because `/` might not *always* produce an integer `2`, and when it doesn't divide exactly, Coalton doesn't force a particular way of rounding. As such, the proper way to do it is divide exactly, then round as you please with `floor`, `ceiling`, or `round`.
Expand Down Expand Up @@ -596,13 +598,13 @@ Lists must be homogeneous. This means the following produces a type error.

```
COALTON-USER> (coalton-toplevel
(define wut (make-list 1 2 3.0)))
Failed to unify types SINGLE-FLOAT and INTEGER
in unification of types (INTEGER → (LIST SINGLE-FLOAT) → :A) and (:B → (LIST :B) → (LIST :B))
in definition of WUT
in COALTON-TOPLEVEL
[Condition of type COALTON-IMPL/TYPECHECKER::COALTON-TYPE-ERROR-CONTEXT]
(define wut (make-list 1.0d0 2.0d0 3.0)))
; error: Type mismatch
; --> repl input:3:4
; |
; 3 | (MAKE-LIST 1.0d0 2.0d0 3.0)))
; | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Expected type '(LIST DOUBLE-FLOAT)' but got '(LIST SINGLE-FLOAT)'
; [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]
```

Lists can also be deconstructed with `match`.
Expand All @@ -622,14 +624,14 @@ Coalton code is statically typechecked. Types are inferred.
```lisp
(coalton-toplevel
(define (fun x)
(map (+ 2) (parse-int x))))
(map (+ 2) (string:parse-int x))))
```

The type of a variable or function can be checked with `coalton:type-of`.

```
COALTON-USER> (type-of 'fun)
(STRING -> (OPTIONAL INT)
(STRING -> (OPTIONAL INTEGER)
```

Type declarations can always be added manually.
Expand All @@ -638,7 +640,7 @@ Type declarations can always be added manually.
(coalton-toplevel
(declare fun (String -> (Optional Integer)))
(define (fun x)
(map (+ 2) (parse-int x))))
(map (+ 2) (string:parse-int x))))
```

Type declarations can also be added in let expressions
Expand Down Expand Up @@ -719,13 +721,19 @@ The into method is used only when a conversion can always be performed from one
((Some (Some x_)) (Some x_))
(_ None)))
;; Literal values can also be matched on
;; Integers or Strings can also be matched on
(define (is-5-or-7 x)
(match x
(5 True)
(7 True)
(_ False))))
(_ False)))
(define (is-five-or-seven x)
(match x
("five" True)
("seven" True)
(_ False))))
```

Functions can pattern match on their arguments, but the patterns must be exhaustive.
Expand Down
4 changes: 2 additions & 2 deletions library/big-float/impl-default.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -352,7 +352,7 @@
((BFNegInf) (error "Cannot rationalize -Inf"))
((BFNaN) (error "Cannot rationalize NaN"))))
(define (best-approx x)
(coalton-library/math/real::rational-approx (get-precision) x)))
(real-approx (get-precision) x)))

(define-instance (Quantizable Big-Float)
(define (proper x)
Expand Down Expand Up @@ -434,7 +434,7 @@
((BFInf) 0)
(_ BFNaN))))

(coalton-library/math/complex::%define-standard-complex-instances Big-Float)
(complex::%define-standard-complex-instances Big-Float)

(coalton-toplevel
;; SeriesSplit/SeriesResult could be extended to any ring (e.g. polynomials)
Expand Down
4 changes: 2 additions & 2 deletions library/big-float/impl-sbcl.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -244,7 +244,7 @@

(define-instance (Real Big-Float)
(define (real-approx prec x)
(coalton-library/math/real::rational-approx prec x)))
(real-approx prec x)))

(define-instance (Rational Big-Float)
(define (to-fraction x)
Expand All @@ -269,7 +269,7 @@
(/ (fromInt a) (fromInt b))
(into (exact/ a b))))))

(coalton-library/math/complex::%define-standard-complex-instances Big-Float)
(complex::%define-standard-complex-instances Big-Float)

(coalton-toplevel

Expand Down
4 changes: 2 additions & 2 deletions library/big-float/package.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,11 @@
(:use #:coalton
#:coalton-library/classes
#:coalton-library/functions
#:coalton-library/math
#:coalton-library/math/integral)
#:coalton-library/math)
(:import-from #:coalton-library/math/dyadic #:Dyadic)
(:local-nicknames
(#:dyadic #:coalton-library/math/dyadic)
(#:complex #:coalton-library/math/complex)
(#:bits #:coalton-library/bits))
(:export
#:RoundingMode
Expand Down
4 changes: 4 additions & 0 deletions library/cell.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -144,6 +144,10 @@
(define-instance (Into (Cell :a) :a)
(define into read))

(define-instance (Into :a String => Into (Cell :a) String)
(define (into c)
(into (read c))))

(define-instance (Default :a => Default (Cell :a))
(define (default) (new (default)))))

Expand Down
6 changes: 6 additions & 0 deletions library/computable-reals/computable-reals.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,12 @@ This threshold is used to ensure `Eq` and `Ord` instances terminate. (In general
(lisp Creal (n)
(cr:/r n)))))

(coalton-toplevel

(define-instance (Dividable Integer CReal)
(define (general/ a b)
(/ (fromint a) (fromint b)))))

(coalton-toplevel

(define-instance (math:Exponentiable Creal)
Expand Down
36 changes: 35 additions & 1 deletion library/lisparray.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,41 @@ WARNING: The consequences are undefined if an uninitialized element is read befo
"Set the `i`th value of the `LispArray` `v` to `x`."
(lisp Unit (v i x)
(cl:setf (cl:aref v i) x)
Unit)))
Unit))

(lisp-toplevel ()
(cl:eval-when (:compile-toplevel :load-toplevel)
(cl:defmacro define-lisparray-specialization (coalton-type lisp-type)
"Specialize lisparray access to known primitive types. This allows the lisp compiler to inline array access."
(cl:let ((ref (cl:intern (cl:format cl:nil "aref/~a" coalton-type)))
(set (cl:intern (cl:format cl:nil "set!/~a" coalton-type))))
`(progn
(specialize aref ,ref (LispArray ,coalton-type -> UFix -> ,coalton-type))
(declare ,ref (LispArray ,coalton-type -> UFix -> ,coalton-type))
(define (,ref v i)
(lisp ,coalton-type (v i)
(cl:aref (cl:the (cl:simple-array ,lisp-type) v) i)))
(specialize set! ,set (LispArray ,coalton-type -> UFix -> ,coalton-type -> Unit))
(declare ,set (LispArray ,coalton-type -> UFix -> ,coalton-type -> Unit))
(define (,set v i x)
(lisp Unit (v i x)
(cl:setf (cl:aref (cl:the (cl:simple-array ,lisp-type) v) i) x)
Unit))))))
)

(define-lisparray-specialization Single-Float cl:single-float)
(define-lisparray-specialization Double-Float cl:double-float)
(define-lisparray-specialization IFix cl:fixnum)
(define-lisparray-specialization UFix (cl:and cl:fixnum cl:unsigned-byte))
(define-lisparray-specialization I8 (cl:signed-byte 8))
(define-lisparray-specialization U8 (cl:unsigned-byte 8))
(define-lisparray-specialization I16 (cl:signed-byte 16))
(define-lisparray-specialization U16 (cl:unsigned-byte 16))
(define-lisparray-specialization I32 (cl:signed-byte 32))
(define-lisparray-specialization U32 (cl:unsigned-byte 32))
(define-lisparray-specialization I64 (cl:signed-byte 64))
(define-lisparray-specialization U64 (cl:unsigned-byte 64))
)

#+sb-package-locks
(sb-ext:lock-package "COALTON-LIBRARY/LISPARRAY")
6 changes: 3 additions & 3 deletions library/list.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
(:local-nicknames
(#:cell #:coalton-library/cell)
(#:iter #:coalton-library/iterator)
(#:arith #:coalton-library/math/arith))
(#:math #:coalton-library/math))
(:export
#:head
#:tail
Expand Down Expand Up @@ -250,10 +250,10 @@
"Returns the nth-cdr of a list."
(cond ((null? l)
Nil)
((arith:zero? n)
((math:zero? n)
l)
(True
(nth-cdr (arith:1- n) (cdr l)))))
(nth-cdr (math:1- n) (cdr l)))))

(declare elemIndex (Eq :a => :a -> List :a -> Optional UFix))
(define (elemIndex x xs)
Expand Down
15 changes: 15 additions & 0 deletions library/math/package.lisp
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
(uiop:define-package #:coalton-library/math
(:use-reexport
#:coalton-library/math/arith
#:coalton-library/math/num
#:coalton-library/math/bounded
#:coalton-library/math/conversions
#:coalton-library/math/fraction
#:coalton-library/math/integral
#:coalton-library/math/real
#:coalton-library/math/complex
#:coalton-library/math/elementary
#:coalton-library/math/dual))

#+sb-package-locks
(sb-ext:lock-package "COALTON-LIBRARY/MATH")
16 changes: 0 additions & 16 deletions library/prelude.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -2,22 +2,6 @@
;;;;
;;;; Collections of packages

(uiop:define-package #:coalton-library/math
(:use-reexport
#:coalton-library/math/arith
#:coalton-library/math/num
#:coalton-library/math/bounded
#:coalton-library/math/conversions
#:coalton-library/math/fraction
#:coalton-library/math/integral
#:coalton-library/math/real
#:coalton-library/math/complex
#:coalton-library/math/elementary
#:coalton-library/math/dual))

#+sb-package-locks
(sb-ext:lock-package "COALTON-LIBRARY/MATH")

(uiop:define-package #:coalton-prelude
(:use-reexport
#:coalton-library/classes
Expand Down
2 changes: 1 addition & 1 deletion library/seq.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
#:coalton-library/classes)
(:local-nicknames
(#:types #:coalton-library/types)
(#:math #:coalton-library/math/integral)
(#:math #:coalton-library/math)
(#:optional #:coalton-library/optional)
(#:cell #:coalton-library/cell)
(#:vector #:coalton-library/vector)
Expand Down
3 changes: 1 addition & 2 deletions library/slice.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,7 @@
#:coalton-library/builtin
#:coalton-library/functions
#:coalton-library/classes
#:coalton-library/math/arith
#:coalton-library/math/integral)
#:coalton-library/math)
(:local-nicknames
(#:types #:coalton-library/types)
(#:cell #:coalton-library/cell)
Expand Down
Loading

0 comments on commit c9ba647

Please sign in to comment.