coalton-lang / coalton Goto Github PK
View Code? Open in Web Editor NEWCoalton is an efficient, statically typed functional programming language that supercharges Common Lisp.
Home Page: https://coalton-lang.github.io/
License: MIT License
Coalton is an efficient, statically typed functional programming language that supercharges Common Lisp.
Home Page: https://coalton-lang.github.io/
License: MIT License
Use serapeum:def
instead of the existing define-global-lexical
code.
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.
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))
...)
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?
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.)
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.
Flat-out error. Bad user! (But make it continuable.)
Error, but only if there are uses of that re-defined variable that conflict.
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)))))
What are the current issues & what would we need to do to implement "overloaded literals"?
See #30
> (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.
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)))))
Currently coalton does not pass tests on ccl in #33. There seem to just be a few small differences that could be fixed easily.
Integer
type (difficulty: distinguishing it from Int
)Single-Float
and Double-Float
compose
($ p q r s)
== (p (q (r s)))
(-> s r q p)
== above ^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.
Instance dicts should not cause undefined variable warnings, and should be available in top level expressions.
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)
.
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?
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.
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))
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?
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
.
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.
Currently typeclass codegen is not very efficient. Here are a series of ideas to improve it.
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.
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.
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))))
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).
It is too easy to not fully apply a function.
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.