Add `define-type-alias` #1294

YarinHeffes · 2024-10-08T23:39:18Z

This is an implementation of type aliases, including:

simple aliases:

(define-type-alias Coordinate Integer)

aliases of aliases:

(define-type-alias Point (Tuple Coordinate Coordinate))
(define-type-alias Translation (Point -> Point))

and readable printing in error messages.

[Point := (Tuple [Coordinate := Integer] [Coordinate := Integer])]

The implementation also supports parametric type aliases

(define-type-alias (UnaryOperator :a) (:a -> :a))
(define-type-alias UnaryIntegerOperator (UnaryOperator Integer))
---
[UnaryIntegerOperator := (UnaryOperator Integer) := (Integer -> Integer)]

Currently, since the does not change types except by substituting type-variables,

(define x (the Coordinate (the Integer 5)))

will compile, but it will not store the alias Coordinate for the variable x, and it will not display in error messages.

The functions describe-type-alias and describe-type-of are implemented to display the definition of a type alias and the aliases of a defined symbol, respectively.

stylewarning · 2024-10-10T19:23:56Z

I think this PR should be blocked on a complete and tested implementation. I am sympathetic to incomplete library additions, but language features need to be complete and bullet-proof.

Izaakwltn · 2024-10-16T21:10:56Z

I think it would be a good idea to add some documentation in these files:

docs/intro-to-coalton.md
docs/coalton-documentation-guide.md
maybe in docs/coalton-lisp-interop.md, if there are any promises (or lack thereof) about lisp alias behavior.

stylewarning

Just some initial thoughts. Not a full review.

docs/coalton-documentation-guide.md

src/faux-macros.lisp

stylewarning · 2024-10-17T05:21:36Z

docs/intro-to-coalton.md

+COALTON-USER> (type-of 'shifted-coordinate)
+(TUPLE INTEGER INTEGER)
+
+COALTON-USER> (describe-type-of 'shifted-coordinate)


I think these functions and their output may need some workshopping.

Do you have any feedback as far as what is good/bad about them?

src/parser/toplevel.lisp

src/typechecker/base.lisp

stylewarning · 2024-10-17T05:30:17Z

@YarinHeffes Can you update the PR description with an up-to-date account of the PR?

stylewarning · 2024-10-17T23:12:17Z

src/parser/toplevel.lisp

+                            "remove unnecessary parentheses")))
+
+       ;; (define-type-alias (name type-variables+) ...)
+       (loop :for vars := (cst:rest (cst:second form)) :then (cst:rest vars)


check that the tyvars are unique

This takes place during the type checking phase, similar to define-struct and define-type

(https://github.com/coalton-lang/coalton/pull/1294/files#diff-ae01ad44c79e0347430c5826a5c355990288337845de14a0bac46c3d601b25efL79)

stylewarning · 2024-10-17T23:17:48Z

src/typechecker/define-type.lisp

+  (let* ((defined-variables (mapcar #'parser:keyword-src-name (parser:type-definition-vars parsed-type)))
+         (used-variables (mapcar #'tc:tyvar-id (tc:type-variables aliased-type)))
+         (unused-variables (loop :for tyvar :in defined-variables
+                                 :when (not (member (tc:tyvar-id (partial-type-env-lookup-var partial-env tyvar parsed-type))


slightly shorted code: when not => unless

addressed in 8619ceb

stylewarning · 2024-10-17T23:22:22Z

src/typechecker/define-type.lisp

+                (tc-note parsed-type "Type alias ~S defines unused type variable~P ~{:~A~^ ~}"
+                         (parser:identifier-src-name (parser:type-definition-name parsed-type))
+                         number-of-unused-variables
+                         (mapcar (lambda (str) (subseq str 0  (- (length str) (1+ (position #\- (reverse str))))))


(position a b :from-end t)

addressed in 8619ceb

stylewarning · 2024-10-17T23:25:27Z

src/typechecker/define-type.lisp

@@ -420,6 +465,12 @@
                                                 `(member ,@(mapcar #'tc:constructor-entry-compressed-repr ctors)))
                                                (t
                                                 name))
+                                :aliased-type (let ((parser-aliased-type
+                                                      (parser:type-definition-aliased-type type)))
+                                                (when parser-aliased-type


prefer if if the value is load-bearing

addressed in 8619ceb

stylewarning · 2024-10-17T23:31:19Z

src/typechecker/predicate.lisp

@@ -69,6 +70,12 @@
  (predicates (util:required 'predicates) :type ty-predicate-list :read-only t)
  (type       (util:required 'type)       :type ty                :read-only t))

+(defun qualified-ty= (qualified-ty1 qualified-ty2)
+  (and (equalp (qualified-ty-predicates qualified-ty1)


what if the predicates have different orders? is that possible?

I would need to look more into this. However, we were previously using equalp for equality, so this change should not break anything/change any pre-existing behavior.

stylewarning · 2024-10-17T23:35:44Z

src/typechecker/types.lisp

@@ -71,7 +74,8 @@
 ;;; Types
 ;;;

-(defstruct (ty (:constructor nil)))
+(defstruct (ty (:constructor nil))
+  (alias nil :type (or null ty-list) :read-only nil))


Describe in a comment what this field is and when it shoes up. Give an example.

maybe a comment that this could be a weak hash table

addressed in 8619ceb

stylewarning · 2024-10-17T23:58:09Z

src/typechecker/types.lisp

+            (tgen-id type2)))
+
+  (:method (type1 type2)
+    (declare (ignore type1)


ignore can have multiple entries: (declare (ignore a b))

addressed in 8619ceb

Jason94 · 2024-12-10T06:12:56Z

src/debug.lisp

+(defun coalton:describe-type-of (symbol)
+  "Print the type of value SYMBOL along with its type aliases and return it"
+  (let ((tc:*pprint-type-aliases* t)
+        (type (tc:lookup-value-type entry:*global-environment* symbol)))


It looks like these are inconsistent with how it prints aliases that are imported from other packages.

If you :use a package then this will print the alias without the package. If you don't :use a package, but do something like this:

(declare adds (aliases2:Int -> Integer -> Integer))

then you will get an error message that does indeed print the package:

--> <macroexpansion>:1:15 | 1 | (COALTON (ADDS "hi" 2)) | ^^^^ Expected type '[ALIASES2:INT := INTEGER]' but got 'STRING'

I think, since this is for debugging purposes, it would be helpful to always print the package that a type is from unless it is from the current package or coalton-prelude. Maybe any of the library functions.

Here is another example. In this error message, we don't :use the package. In the error message, the alias is printed with one : but the type it refers to (from the same package) is printed with two ::'s:

"aliases2"

(in-package :cl-user) (defpackage :aliases2 (:use #:coalton #:coalton-prelude) (:export :Int :Ham :Swiss :Cheese)) (in-package :aliases2) (coalton-toplevel (define-type MoldyMilk Ham Swiss) (define-type-alias Cheese MoldyMilk)) (coalton-toplevel (define-type-alias Int Integer))

aliases (main package)

(in-package :cl-user) (defpackage :aliases (:use #:coalton #:coalton-prelude)) ;; #:aliases2)) <---- not using the other package (in-package :aliases) (coalton-toplevel (declare value-of-cheese (aliases2:Cheese -> Integer)) (define (value-of-cheese chs) (match chs ((aliases2:Ham) 10) ((aliases2:Swiss) 20)))) (coalton (value-of-cheese "not cheese"))

error: Type mismatch --> <macroexpansion>:1:26 | 1 | (COALTON (VALUE-OF-CHEESE "not cheese")) | ^^^^^^^^^^^^ Expected type '[ALIASES2:CHEESE := ALIASES2::MOLDYMILK]' but got 'STRING'

I will take a closer look at the behavior of describe-type-of. But regarding your examples, I believe those are all expected behaviors.

First, the use of : versus :: depends on whether is a symbol is exported. If a package p exports a symbol s, and you do not want to :use package p, then you can use the symbol with p:s. If p does not export s, then you can still use it with p::s. In your example, aliases2 exports cheese but not moldymilk.

Second, when package p :uses package q, the symbols from q receive the same treatment locally, in p, as any other symbol defined in p, so my personal opinion is that it is not inconsistent for those types aliases to be printed without the q: prefix.

That makes sense 👍

Jason94 · 2024-12-10T06:18:01Z

tests/test-files/define-type-alias.txt

@@ -0,0 +1,142 @@
+================================================================================
+1 Define type alias


Should add tests around package boundaries. Permutations that come to mind:

use an alias for a standard type from another package that has been imported with use

Reference an alias for a standard type from another package without :use

Both of the above to a type that is from the same package but was not exported.

Both of the above, but the alias in package 2 is to a type from a third package which is not :used in the main package

Jason94 · 2024-12-10T06:32:34Z

Testing uninterning aliases, if you:

Point alias A -> a type, and point alias B -> alias A
then unintern A

B will still continue to function. You can use it to define new type signatures - works just fine. The error message you get looks like this:

Note the #:A instead of A:

error: Type mismatch
  --> <macroexpansion>:1:18
   |
 1 |  (COALTON (BAD-ADD "hi" 2))
   |                    ^^^^ Expected type '[B := #:A := INTEGER]' but got 'STRING'

This seems like reasonable behavior, so much as anything would be. This (hopefully) won't come up much, but it's worth verifying that it doesn't crash everything if it does.

Here is some code to play around with this:

(coalton-toplevel
  ;; (define-type-alias A Integer)
  ;; (define-type-alias B A)

  ;; (declare a-add (A -> A -> Integer))
  ;; (define a-add +)
 )

(coalton-toplevel
  (declare bad-add (B -> B -> Integer))
  (define (bad-add b1 b2) (+ b1 b2)))

(coalton (bad-add 1 2))
(cl:unintern 'A)

YarinHeffes and others added 6 commits October 7, 2024 16:39

added basic define-alias toplevel form

758cf3d

fixed alias substitution for constructors and struct-fields

a125e4a

added alias tests

074488b

improved alias error messages

688322c

removed with-aliases-from

287f089

Merge branch 'coalton-lang:main' into type-alias

77a2443

YarinHeffes requested review from jbouwman and eliaslfox October 8, 2024 23:39

YarinHeffes mentioned this pull request Oct 8, 2024

Add Type Aliases #912

Open

alias coalton-release fix

e05bd8a

YarinHeffes marked this pull request as draft October 10, 2024 20:12

YarinHeffes added 4 commits October 16, 2024 11:38

added parametrized type aliases

db74f65

added tests for parametrized type aliases

ffbef6e

added describe-alias

f252499

added define-alias.txt tests

9dda5c2

YarinHeffes added 3 commits October 16, 2024 14:25

add tutorial documentation for type aliases

314ff0b

added type alias documentation guide

fde68b5

Merge branch 'main' into type-alias

c9ba647

YarinHeffes marked this pull request as ready for review October 16, 2024 21:58

stylewarning requested changes Oct 17, 2024

View reviewed changes

YarinHeffes added 4 commits October 17, 2024 09:45

removed empty line

5851da6

changed :nil to nil

ff0e7f7

added documentation to *pprint-aliases*

9b3beda

changed define-alias -> define-type-alias

57366b7

YarinHeffes changed the title ~~adding define-alias~~ adding define-type-alias Oct 17, 2024

YarinHeffes changed the title ~~adding define-type-alias~~ Add define-type-alias Oct 17, 2024

Improved error message for unused type alias arguments

1aba695

typo fix

e6784b8

stylewarning requested changes Oct 18, 2024

View reviewed changes

minor fixes

8619ceb

Jason94 reviewed Dec 10, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add `define-type-alias` #1294

Add `define-type-alias` #1294

YarinHeffes commented Oct 8, 2024 •

edited

Loading

stylewarning commented Oct 10, 2024

Izaakwltn commented Oct 16, 2024

stylewarning left a comment

stylewarning Oct 17, 2024

YarinHeffes Oct 17, 2024

stylewarning commented Oct 17, 2024

stylewarning Oct 17, 2024

YarinHeffes Nov 19, 2024

Jason94 Dec 10, 2024

stylewarning Oct 17, 2024

YarinHeffes Nov 19, 2024

stylewarning Oct 17, 2024

YarinHeffes Nov 19, 2024

stylewarning Oct 17, 2024

YarinHeffes Nov 19, 2024

stylewarning Oct 17, 2024

YarinHeffes Nov 19, 2024

stylewarning Oct 17, 2024

stylewarning Oct 17, 2024

YarinHeffes Nov 19, 2024

stylewarning Oct 17, 2024

YarinHeffes Nov 19, 2024

Jason94 Dec 10, 2024

YarinHeffes Dec 10, 2024

Jason94 Dec 10, 2024

Jason94 Dec 10, 2024

Jason94 commented Dec 10, 2024

		@@ -0,0 +1,142 @@
		================================================================================
		1 Define type alias

Add define-type-alias #1294

Are you sure you want to change the base?

Add define-type-alias #1294

Conversation

YarinHeffes commented Oct 8, 2024 • edited Loading

stylewarning commented Oct 10, 2024

Izaakwltn commented Oct 16, 2024

stylewarning left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

stylewarning commented Oct 17, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Jason94 commented Dec 10, 2024

Add `define-type-alias` #1294

Add `define-type-alias` #1294

YarinHeffes commented Oct 8, 2024 •

edited

Loading