carp-lang / carp-lang/Carp

[Proposal] Strong and weak aliases

Open
#884 5 comments 0 reactions 0 assignees View on GitHub
nice-to-have under discussion
Dominant language
Haskell
Stars
6k
Forks
187
Avg merge
8d 22h
Merged PRs (30d)
4

Description

# Strong Aliases

It'd be convenient to resurrect `defalias` and allow programmers to define other names for types. This doesn't change much functionally, but it would save one some keystrokes.

A "strong" alias is nothing more than another name for a type, with no additional effects on inference, etc. That is, assuming we have a type `t` and an alias for that type `a`, `t` and `a` may be used interchangeably and the type system will not complain. Aliases should support type variables so that they may be used to alias polymorphic types.

Since strong aliases and the types they alias are directly interchangeable, one may use values of the original type in an aliased position without issue.

```
(defalias Ints (Array Int))

(sig head (Fn [Ints]) Int)
(head [1]) ;; still works, since (Array Int) and Ints are interchangeable
```

# Weak Aliases

In addition to strong aliases, I propose we also support "weak" aliases, which are a slightly more complicated mechanism but also augment type-level programming.

Unlike a strong alias, a weak alias is not directly interchangeable with the type it aliases and is a different type from the perspective of the type system. Just like other types, it introduces a constructor and signatures that expect a weak alias `w` for some type `t` will not accept `t`. Weak aliases should only admit a single constructor. In this respect, they are somewhat analagous to Haskell's `newtype`s.

```
(defweak Ints (Ints [(Array Int)]))
(sig head [Ints] Int)
(head [1]) ;; ERROR! (Array Int) is not the same as `Ints`!
(head (Ints.Ints [1])) ;; good
```

So, how are weak aliases weak? Well, the essential idea behind them is that they *do not emit new code*--for a given weak alias, all of its emissions resolve to the underlying aliased type. In a sense, a weak alias is a distinction that lives at type level only, allowing programmers to write more precise program specifications without incurring the runtime cost of an actual type definition.

Example use case:

Carp's type system is already expressive enough to simulate some amount of "dependent types". Consider the following:

```
(deftype Zero)
(deftype (Succ a) (Succ [a]))
;; "pseudo-dependent type for arrays"
(deftype (Vector n a) [of (Array a)])

(sig tail (Fn [(Vector (S (S n)) (Array a))] (Vector (S n) (Array a))))
```

This set of types has the intended effect of verifying that a function like `tail` returns a `Vector` that has a length its `n` argument of one lesser than the input `Vector` -- we represent lengths as nested `S` types, where the final type will be `S Zero` (e.g .`(S (S (S Zero)))`).

This works great! The only issue is, it incurs extra costs in our program since we need to define a new type, give it a constructor etc. even though the additional information is held in a phantom type `n` that we never use! The benefits to this set up happen purely at type level--at run time `Vector` might as well just be an array, yet currently we cannot avoid the extra costs that come with defining a new type, even though that type is only relevant to the type checker.*****

With a "weak" alias, we could define such a type and *guarantee* that it won't cost us in the form of extra emitted code.

```
(deftype Zero)
(deftype (Succ a) (Succ [a]))
;; "pseudo-dependent type for arrays"
(defweak (Vector n a) (of [(Array a)]))

(sig tail (Fn [(Vector (S (S n)) (Array a))] (Vector (S n) (Array a))))
```

This time, `Vector` is purely a type-level construct, it has no values, no concrete inhabitants. The type checker would ensure that all things that expect a `Vector` get a `Vector` but just before emission time, all cases of `Vector` will be replaced with the appropriate emission for normal, plain old arrays.

I'm not sure if `weak alias` is really the right name for this sort of thing, but I'm not sure what else to call it. Perhaps `psuedo-type`?

*****: Note that this isn't *really* a dependent type system, it is "dependent types on good faith". A cruel programmer could still define tail such that the underlying `Array` actually *incremented* its length rather than decrementing it. So, it does not grant one the full benefits of a dependent type system, it only simulates some of the effects of such a system. Then again, the direct implementation of a dependent type system also relies on some amount of good faith (we trust compiler authors to follow the same value ordering schemes as we do)

Contributor guide

Open the contributing guide

Research direction

The proposal names no files, tests, or compiler entry points. Begin by locating Carp's type-checking and code-emission paths, then determine how strong and weak aliases would be represented and erased; done means aliases support the described typing behavior without extra emitted code.

Written by the indexing model from the issue text.

Assessment

Tech stack
haskell
Domain
compilers
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
20/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.