Influences

Some languages have been inspiring when building Pikelet. We list some of them here, and the contributions they have made in our thinking. These ideas may or may not be included in the final Pikelet language, but they are worth mentioning!

Contents

1ML

Links:

Key things we love:

  • focus on simplicity
  • combines module language of ML with dependent records
  • formalized foundation

Agda

Links:

Key things we love:

  • interactive editing
  • dependent types
  • dependent records
  • implicit arguments
  • instance arguments for emulating type classes
  • codata for unbounded data
  • totality checking
  • inductive data types

ATS

Links:

Key things we love:

  • dependent types
  • proofs can be generated by SMT solvers
  • high level of performance, low level interoperability
  • unboxed data types

D

Links:

Key things we love:

  • strong support for static metaprogramming
  • design by introspection (ie. breaking parametricity for performance optimization and metaprogramming purposes)
  • low-level control and high-level abstraction
  • fast compiler, short iteration times

Dhall

Links:

Key things we love:

  • simple core language
  • dependent types
  • total language
  • structural records

Discus (formerly DDC)

Links:

Elm

Links:

Key things we love:

  • focus on usability, and adoption
  • friendly marketing
  • welcoming community
  • best-in-class error messages
  • row polymorphism

F*

Links:

Key things we love:

  • combining SMT solvers with explicit proofs
  • combining effects with dependent types

Gluon

Links:

Key things we love:

  • strict evaluation
  • focus on simplicity
  • embeddable in Rust programs
  • using records as a basis for the module system

Granule

Links:

Key things we love:

  • combining coeffects with effects in one language

Idris

Links:

Key things we love:

  • focus on making dependently typed programming practical
  • interactive editing
  • simple core type theory
  • opt-out totality checking
  • nice, accessible documentation, focused on real-world examples
  • universe checking
  • aggressive erasure
  • linear types
  • compilation to native code
  • elaborator reflection
  • ad-hoc interfaces desugar into records
  • effects system as a library
  • state machine library

Ivory

Links:

Koka

Links:

Key things we love:

  • algebraic effects and handlers
  • nice library documentation, with clickable links, etc.

Lean

Links:

Key things we love:

  • focus on responsive interactive development
  • metaprogramming support using Lean
  • simple kernel language

OCaml

Links:

Key things we love:

  • module system
  • algebraic effects
  • modular implicits
  • row polymorphism
  • structural records
  • efficient (and fast) code generation

Rust

Links:

Key things we love:

  • friendly community
  • non-uniform, unboxed data layout
  • predictable optimizations
  • focus on systems programming
  • having safety and low level code under one roof
  • infectious 'unsafe' keyword
  • strict evaluation
  • opt-in garbage collection
  • minimal runtime
  • bootstrapped itself off a foundation of C libraries

Sixten

Links:

Key things we love:

  • non-uniform, unboxed data layout
  • dependent types

Ur

Links:

Key things we love:

  • Statically typed metaprogramming with type-level records