coalton-lang/coalton

Coalton is an efficient, statically typed functional programming language that supercharges Common Lisp.

coalton's Issues

Proposal: Allow defining overlapping instances?

The following instances currently would cause overlap issues. However being able to define them would be very useful.

(coalton-toplevel
  (define-instance ((Into :a :c) => (TryInto :a :b :c))
    (define (tryInto x)
      (Ok (into x)))

   (define-instance ((Into :a :b) (Into :b :c) => (Into :a :c))
      (define (into x) (into (into x)))))

Rewrite check-variables

See #30

Should nullary function *syntax* be shorthand for applying to `Unit`?

If we adopt a convention that

(declare f (Unit -> Foo))

represents something stateful or perhaps allocating in nature (e.g., creating a fresh object like a vector), then maybe it’s nice to have a syntax that is Lispy, like

(f)

which at parse-time is rewritten

(f Unit)

Thoughts?

Predicates being dropped on top-level variable

The predicates for top level variables are being dropped leading to incorrect codegen:

(declare test (List Int))
(define test mempty)

Output code:

(COALTON-IMPL::DEFINE-GLOBAL-LEXICAL TEST MEMPTY)

Expected:

(COALTON-IMPL::DEFINE-GLOBAL-LEXICAL TEST (A1 |MONOID LIST| MEMPTY))

This seems to only happen in explicitly bound variables that would otherwise face the monomorphism restriction (if implicit).

CCL Support

Currently coalton does not pass tests on ccl in #33. There seem to just be a few small differences that could be fixed easily.

Apply substitutions to definitions outside of the current compilation unit

Setup Website

Add unused variable warning

Implement GHC’s `SPECIALIZE` pragma

Here contains the description of it.

See also this.

Double check library functions are exported

Audit calls to MAPCAN, possibly replace them with something safe-by-default

MAPCAN is an easy source of bugs, even if the original users of MAPCAN knew what they were doing. Lots of methods use MAPCAN extensively, and if a programmer adds a new method that doesn't use MAPCAN and doesn't make a fresh list, the code will be very subtly buggy.

We should first audit calls to MAPCAN (at the time of writing there are around 20 of them), and second decide if we should replace them with safe versions. Something like:

(defun mappend (f list &key (unsafe nil))
  "Apply F (which ought to return a list) to each element of LIST and append the results. If UNSAFE is T, then the intermediate lists may be mutated."
  (cond
    (unsafe
     (loop :for x :in list
           :nconc (funcall f x)))
    (t
     (loop :for x :in list
           :append (funcall f x)))))

Intro Doc

Add `coalton` macro

Add coalton macro which evaluates a coalton expression. This would be useful in the repl when trying to debug coalton code and could also appear as another way to interop from lisp to coalton.

Predeclare Instance Dicts

Instance dicts should not cause undefined variable warnings, and should be available in top level expressions.

Case Exhaustiveness Checking

Review docs folder and add docs/README.md

Put library code into `COALTON-LIBRARY` and keep `COALTON-USER` "clean"

I think @eliaslfox was on the right track with a separate package in previous commits. I think we should do this, and not pollute COALTON-USER.

Explicit bindings in LET blocks

Pointfree Transform

Transform the following code

(define f
  (map (+ 1))

Into this code

(define (f xs)
  (map (+ 1) xs))

This will reduce closures and allow for more direct calls.

Finish core standard library functionality

Numeric Types

• Integer type (difficulty: distinguishing it from Int)
• Single-Float and Double-Float

Strings

• Concatenation "story" should be improved

Functions

• compose
• application syntax ($ p q r s) == (p (q (r s)))
• threading syntax (-> s r q p) == above ^

Coalton `APROPOS` for searching for types/values/etc.

Can we implement "Overloaded X" for X in {Integer, String, ...}?

What are the current issues & what would we need to do to implement "overloaded literals"?

How should type-incompatible re-definitions work?

Consider this:

COALTON-USER> (coalton-toplevel
                (define (f x) 5))
F
COALTON-USER> (coalton-toplevel
                (define (f x) "x"))
COMMON-LISP:WARNING: redefining COALTON-USER::F in DEFUN
F

Lisp is OK allowing this redefinition even though the type changes. How should we handle this?

Option 1

Do nothing. Just keep the behavior as-is.

This is maximally Lispy, but defeats some of the point of Coalton. I actually ran into this problem of THIH silently overwriting COMPOSE. (Would have been solved with a package lock.)

Option 2

Issue a warning that a function is re-defined with a different type. This will make compilation units error if redefinition happens, but REPL interactions OK.

Option 3

Flat-out error. Bad user! (But make it continuable.)

Option 4

Error, but only if there are uses of that re-defined variable that conflict.

Check for self recursive variables

The following code will typecheck but will not codegen properly because variables cannot be self recursive.

(declare-type (WrapFunction :a :b)
  (WrapFunction (:a -> :b))

(declare unwrapFunction ((WrapFunction :a :b) -> (:a -> :b))
(define (unwrapFunction w)
  (match w
    ((WrapFunction f) f)))

(define f
  (WrapFunction (fn (a)
    (if (== a 2)
      3
      ((unwrapFunction f) 2))))

(define g ((unwrapFunction f) 1))

Default Typeclass Methods

Setup CI

(fromSome "" (vector-index (into idx) ...))

check-type needs to be reenabled

Variable renaming breaks constructor name overlapping warning in match expressions

Get Logo

THIH fails to load

Proposal: mAkE cOaLtOn CaSe SeNsEtIve

Instance INTO #T3208976 (CELL #T3208976) overlaps with instance INTO #T1143 #T1143

Switch to serapeum:def

Use serapeum:def instead of the existing define-global-lexical code.

Let Flattening

Let bindings tend to form a dependency chain in real code. This will create a series of dependent sccs which will then be codegened into a series of nested let expressions.

These sccs could be flattened into a smaller number of sccs which will then generate less code.

Untabify entire project

There seem to be a lot of tabs still hiding in the files in this project. We need to run through and replace them with spaces.

Interfacing w/ Lisp Guide

Only declare local functions in the variable namespace when they are referenced there

How do we implement `Ratio` and `Complex`?

There is difficulty in implementing these as native Lisp objects, because:

• Problem 1: reduction of #C(k 0) to k; or k/1 to k

• Problem 2: Lisp doesn't allow arbitrary field elements as components (Complex :a cannot use Lisp's complex numbers)

How do we implement Complex Single-Float as specialized on (COMPLEX SINGLE-FLOAT), but also allow Num :a => Complex :a to exist?

Design Decisions Doc

Coalton's type system is unsound in the presence of mutation

Coalton currently uses a type system based on Hindley-Milner type classes added. This is unsound in the presence of mutation as shown by the following example.

(coalton-toplevel
  (define _
    (progn
      (let v = (make-vector))
      (vector-push 5 v)
      (vector-push "hello" v)
      (traceObject "vector" v)))) ;; vector: #.(VECTOR #<LISP-OBJECT #(5 "hello")>)

In Haskell mutation is only allowed in the IO monad making this a nonissue.

In coalton however mutable values can be defined in let expressions. In the above example the type of v is (Vector :a). This allows v to be used in both calls to vector push which are typed as (Integer -> (Vector Integer) -> Unit) and (String -> (Vector String) -> Unit) respectively. For the above code to be type safe the first call of vector-push must change the type of v to (Vector Integer).

A somewhat similar feature already exists in the language in the form of the monomorphism restriction. The following code does not type check.

(coalton-toplevel
  (define _
    (progn
      (let eql = ==)
      (eql 5 5)
      (eql "hello" "hello"))))

;; Failed to unify types STRING and INT
;; in unification of types (STRING → STRING → :A) and (INT → INT → BOOLEAN)
;; in definition of _
;; in COALTON-TOPLEVEL

When a definition of a variable in a let expression has non static predicates, then the variables in those predicates are resolved to their first usage. In the above example the type of eql is FORALL. :A -> :A -> Boolean, if it was defined as a function and thus not subject to the monomorphism restriction that its type would be FORALL A. :A -> :A -> Boolean.

The monomorphism restriction only looks at the types of bindings, however that would be insufficient to correctly type check the following example.

(coalton-toplevel
  (define _
    (progn
      (let v = (make-vector))
      (let f = (fn (x) (vector-push x v)))
      (let g = (fn (x) (vector-push x v)))
      (f 5)
      (g "hello")
       v)))

From this example it is clear that calling f must change the type of v to (Vector Integer). This type system feature exists in Ocaml and is documented here.

Typeclass Codegen Ideas

Currently typeclass codegen is not very efficient. Here are a series of ideas to improve it.

Lift Static Constructed Dictionaries to a global scope

Typeclass instances without constraints are compiled into instances of a struct while instances with constraints are compiled into functions that return a struct.

(declare f (Int -> Int -> Boolean))
(define (f a b)
  (== a b))

(declare g (Result String Int -> Result String Int -> Boolean))
(declare (g a b)
  (== a b))

(defun (f a b)
  (== |INSTANCE/EQ INT| a b))

(defun (g a b)
  (== (|INSTANCE/EQ (RESULT :A :B) |INSTANCE/EQ STRING| |INSTANCE/EQ INT) a b))

If the Eq dictionary for Result String Int was lifted then the codegen could look something like this

(define-global-lexical #:G402 (== (|INSTANCE/EQ (RESULT :A :B) |INSTANCE/EQ STRING| |INSTANCE/EQ INT) a b))

(defun (g a b)
  (== #:G402 a b))

This would construct the dictionary once instead of constructing it every time that g is called.

Transform calls to typeclass methods to direct function calls

Currently method calls on static dictionaries are compiled as shown below

(defun (a b)
  (+ |INSTANCE/NUM INT| a b))

They could be compiled instead to

(defun (a b)
  (|+-INSTANCE/NUM INT| a b))

This would allow sbcl to much better optimize the call site.

Hoist constructed dictionaries to a higher scope

Currently if a constructed dictionary is used multiple places in a function it will be constructed multiple times.

(declare f ((Result :a :b) -> (Result :a :b) -> (Tuple Boolean Boolean))
(define (f a b)
  (Tuple (== a b) (/= a b)))

The above coalton code would be compiled into the following code

(defun (f #:G401 #:G402 a b)
  (Tuple 
    (== (|INSTANCE/EQ (RESULT :A :B)| #:G401 #:G402) a b)
    (/= (|INSTANCE/EQ (RESULT :A :B)| #:G401 #:G402) a b)))

It could instead be compiled to the following code

(defun (f #:G401 #:G402 a b)
  (let ((#:G403 (|INSTANCE/EQ (RESULT :A :B)| #:G401 #:G402 )))
    (Tuple (== #:G403 a b) (/= #:G403 a b))))

Cannot open-code type checks when loading THIH

> (asdf:load-system :thih-coalton :force t :verbose t)
...
...
; ==>
;   (THE THIH-COALTON:KIND THIH-COALTON::|_1|)
; 
; note: can't open-code test of unknown type KIND
...
...

It sounds like types aren't known by the time they're needed by the compiler to produce more efficient code.

Add package lock to standard library

LISP forms don't properly rewrite variables

Make Show instances set the pprint method

Add "newtype" functionality

We should add Haskell-inspired newtype functionality, which allows us to create a "cheap" type abstraction that gets type checked but has no runtime penalty.

I'm not sure what the syntax should be but assuming it's

(define-newtype (F :t1 :t2 ...) (F ty))

then (F s1 s2 ...) would be a type whose representation is runtume-equivalent to ty[:ti = si]. This means that the constructor function #'F would just be identity (and ought to be inlined, since it can still be used as a high-order function).

I think codegen would be trivial (i.e., do nothing), except in the case of codegenning match, which must just be a let-rebinding, since runtime-type inspection can't happen:

(match outer
  ((Foo inner) ...))

; ==>

(let ((inner outer))
  ...)

Deriving mechanism

Add a warning when a form in a seq returns a function type

It is too easy to not fully apply a function.

Instance dict undefined when simultaneously defining instances and top-level variables

Repro:

(coalton-toplevel
  (define-type Foo Foo)
  (define-instance (Eq Foo)
    (define (== a b) True)
    (define (/= a b) False))
  (define yes (== Foo Foo)))

Results in

The variable COALTON-USER::|INSTANCE/EQ FOO| is unbound.
   [Condition of type COMMON-LISP:UNBOUND-VARIABLE]

probably when attempting to evaluate (== Foo Foo).