maxdesiatov/typology

Swift type checking and semantic analysis for developer tools

Typology

Typology is a work in progress attempt to implement type checking of Swift in Swift itself. Currently it uses SwiftSyntax as a parser, but is ready to switch to other pure Swift parsers in the future when any are available.

Goals

• Education: understanding how type checking can be implemented in a Swift compiler
• User Experience: finding the best way to report type errors and to improve related developer tools
• Research and Experimentation: prototyping advanced features that could be fully developed within Swift's type system.

How does it work?

Same as the type checker in Apple's Swift compiler, Typology relies on the fact that you can express type systems with a set of constraints on types that are resolved through unification.

See also

Type systems and type checkers

• Apple's Swift Compiler Type Checker Design and Implementation by multiple contributors
• A Type System From Scratch by @CodaFi
• Write You a Haskell: Hindley-Milner Inference by @sdiehl
• Typing Haskell in Haskell by Mark P Jones
• “What part of Hindley-Milner do you not understand?” question and answers on StackOverflow
• So you want to write a type checker... by @psygnisfive
• Exponential time complexity in the Swift type checker by @mattgallagher
• A Swift Playground containing Martin Grabmüller's "Algorithm W Step-by-Step" by @CodaFi

Error reporting

• Compiler Errors for Humans on Elm blog
• Shape of errors to come in Rust compiler by Jonathan Turner

Optimizing type checker's performance for large projects

• Apple's Swift Compiler Dependency Analysis by multiple contributors

typology's Issues

Basic AST types

• Simple literal expressions
• Ternary expressions
• Identifier expressions
• Function applications
• Variable and constant declarations
• Closure expressions
• Value members of struct declarations
• Compound literal expressions (arrays, dictionaries, string interpolations)
• Operators (represented as simple function applications in AST)
• Simple function declarations with concrete types
• protocol declarations
• Generic function declarations with protocol constraints
• as operator
• as! operator
• as? operator
• Explicit signatures
• Existential types
• Static members of struct declarations
• enum declarations

Support Markdown doc comments in LSP

It's unclear yet whether this should be implemented in Typology module itself, or TypologyLSP module. I'm inclined to do the former, as this would allow to do semantic checks against doc comments (number of parameters and their names) and make doc comment auto-complete suggestions with parameter names auto-filled.

Support function overloads

A test case that should pass type checking:

func f(x: Int) -> Int { return 42 }
func f(x: String) {}
func f(x: Double) -> Double { return 42.0 }

let x = 42 + f(x: 42) // `x` inferred to be `Int`
let y = 42.0 + f(x: 42.0) // `y` inferred to be `Double`

Distinguish between "common" and "scripting" modes

In "scripting" mode AST should preserve the order of top-level declarations, which probably means using different AST types and name resolution rules. On the top level the AST would probably be just an array of nodes, each can be either a declaration or an expression:

protocol ScriptNode {
}

extension Expr: ScriptNode {}
extension Decl: ScriptNode {}

typealias ScriptFile = [ScriptNode]

Support extensions

While all extensions would be merged into the same environment during typechecking, AST should have a separate type for extension nodes. Existence of members in the main type declaration, as compared to extension members, triggers different semantic checks, e.g. synthesized memberwise initializers etc. Besides, extensions can have predicates on them, which would also be represented on extension AST nodes.

This issue also requires the environment "transformer" mentioned in #19, that converts AST to environment, should also take extensions into account somehow. Maybe there should be a separate Environment type with mutating functions that can consume AST and modify the environment during AST traversal?

Type check throwing expressions and closures

Check for duplicate declarations and members

This includes checking overlapping extensions in #21.
This should still allow function overloads to exist.
Typealiases implemented in #31 should also be taken into account.

Build environment from non-generic function declarations

Function declarations AST is already working more or less. Now var environment: Environment can be defined on File type to transform its AST into an environment that can be passed into ConstraintSystem initializer in tests that verify this.

Support default function arguments

This requires AST -> Environment transformation to check for overlapping overloaded declarations and to generate new overloads based on possible applied default arguments.

Support generic enums

This is blocked by #7

Support string interpolation

Implement dependency analysis for efficient rechecks of big projects

Implement diagnostic infrastructure

This requires #25 to be fully implemented.

Diagnostic infrastructure should be able to report errors, warnings and supporting informations in different formats: terminal output, LSP format, potentially Xcode format.

Types of diagnostic:

• Error
• Warning
• Suggestion (fix-it)
• Explanation (should probably be emitted only in a special "explanation" mode)

Note that diagnostic is separate from logging, since logging produces internal information useful for debugging, while diagnostic messages are redirected separately through either LSP, REPL, or plain terminal output coming from "batch" typology File.swift invocations.

Support navigating to declarations

Support for shadowed and overloaded declarations is also required.

Implement name resolution across a module in LSP

Implementing this requires #11 to be ready for use.

Implement inference for multi-parameter closures

Currently Expr values are able to represent only single-parameter closures with case lambda(Identifier, Expr). The simples way to implement multiple parameters would be to change that to case lambda([Identifier], Expr) and match that value accordingly within the switch in the infer function by generating a fresh type variable for each identifier, passing those to infer(inExtendedEnvironment:) function. Additional tests for the new behaviour also need to be implemented.

Support static members

Implement REPL CLI command

A simple typology command should launch a new REPL instance that's ready to parse given Swift code and build an environment from it.

repl command should allow invocations of the form typology repl File.swift that parses the file and starts a REPL with all declarations in that file already available in scope.

So far it looks like Linenoise library would be the best option to try at first for the REPL implementation.

Implement tuple element names in AST and inference

Tuple element names are formally described in the language reference.

Support generic struct declarations

This implies AST support for following declarations:

struct Array<Element> {
  var count: Int
  var first: Element?
}

There should also be a property (or function) on the corresponding struct AST type that transforms a value of this type to a [TypeIdentifier: Environment] dictionary.

Support `as` operator and explicit signatures

The simplest use case is support for Any subtyping, but we also need to support existential types in the future, such as

protocol P {}
extension Int: P {}
let x = 5 as P

After handling of as is implemented, we would be able to handle explicit signatures properly:

let x: P = 5

by internally converting this declaration to AST that's equivalent to let x = 5 as P.

Support tracking source location for error reporting

This requires adding var position: AbsolutePosition { get } property to the Statement protocol. AbsolutePosition is defined in the SwiftSyntax module. enum Expr should no longer conform to Statement, but should be wrapped as a property of struct ExprNode: Statement, which would allow attaching position to expressions. Other types conforming to Statement will require adding let position: AbsolutePosition stored property to them.

Support typealias declarations

A typealias probably should be desugared before building an environment, but it should be preserved somehow to keep diagnostics useful.

Implement CLI executable with simple diagnostic output

A simple invocation of typology File.swift should run type checking on the file and report any errors that were found.
SwiftCLI seems to be an obvious candidate for the command-line arguments and commands parsing.

Support generic function declarations

Inference and type checking within functions such as

func max<T: Comparable>(_ x: T, _ y: T) -> T {
  return x > y ? x : y
}

can be implemented with a creation of a "fake" concrete type T, which has all members of Comparable protocol copied into it. Then inference of func max could run as if T is a type constructor of a concrete type, not a generic parameter.

Implement LSP command in CLI executable

This requires #27 to be fully implemented.

CLI invocation of the form typology lsp should start an LSP server listening on some default port. This server should be able to typecheck isolated files and provide name resolution for declarations defined in those files. Resolving declarations across files and modules would be implemented as a part of a separate issue.

We can reuse the existing LanguageServerProtocol module in sourcekit-lsp. I'm linking to a fork as we will still need to make that module importable in Typology by defining it as a product in our fork.

To test the server, it makes sense to build a simple VS Code extension as described in Language Server Extension Guide. In the first implementation, we can start with supporting only DidSaveTextDocument notification to type check the opened file when it's saved and emit diagnostics for discovered errors.

Support pattern matching

This implies supporting both pattern matching in switch statements, and if case let bindings.

Support subscript expressions

Refactoring support

This most probably depends on #26 to track all uses of a particular symbol throughout the opened package.