• Stars
    star
    189
  • Rank 199,916 (Top 5 %)
  • Language
    Haskell
  • License
    GNU Affero Genera...
  • Created over 5 years ago
  • Updated about 1 year ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

An implementation of Pie in Haskell

Pie in Haskell

This is an implementation of Pie, the language from The Little Typer, in Haskell.

How to Use It

Compile the program with cabal v2-build. Run the tests with cabal v2-test. Once it works, use cabal v2-install to install the binary somewhere. Alternatively, you can use the stack build, stack test, and stack install commands.

This implementation of Pie can be run in two modes:

  • An interactive REPL
  • A batch-mode processor

To start the REPL, invoke pie without a filename as an argument. To process a Pie file in batch mode, use pie FILENAME.

To learn Pie, please consult The Little Typer. If you need to refresh your memory, please consult the language reference.

REPL Commands

An expression
Expressions are treated as examples to be type checked and evaluated.
A declaration
Declarations, such as claims, definitions, and check-same forms, are treated as if they were in a file. Claims and definitions are added to the context, and check-same checks sameness immediately.
:verbose
Switch Pie to verbose mode.
:concise
Switch Pie to concise mode.
:load FILE
Load FILE, throwing away the current context.

Concise and Verbose Modes

In concise mode, Pie emits only the information about the user's program that is explicitly requested. In other words, it will display error messages and the explicit results of examples that the user has requested.

In verbose mode, Pie additionally displays information about the type of each subexpression that it successfully checks. While this information could serve as the basis for a good editor plugin, this has not yet been implemented.

Readline support

The REPL in this implementation of Pie does not support arrow keys or other similar features. You can get rudimentary support for them using rlwrap.

Relationship to the Racket implementation

I wrote this implementation so that people who know Haskell but not Racket would be able to read it and understand how the internals work. This one is probably not as nice to experiment with and/or use as the version written in Racket, as that version has many useful features in DrRacket, including tooltips on every expression showing its type, a pop-up list of TODOs, arrows from variables to their binding sites, auto-indentation support, "go to definition", and automatic renaming of variables. This version is just a batch-mode type checker and REPL.

Design Guidelines

This implementation of Pie is intended to be as clear and simple as possible. Clarity and simplicity are more important than performance, but less important than correctness. To help achieve this, the code adheres to the following dogmas:

  1. As few dependencies as possible - currently just base and text. More dependencies are allowed in the test suite.
  2. Absolutely no language extensions. Haskell 2010 only.
  3. No monad transformers.

Compiler and Library Support

Because it relies on Data.List.NonEmpty, this package requires at least GHC 8.0.1.

More Repositories

1

idris-type-providers

Type provider library for Idris
Idris
85
star
2

idris-quickcheck

A port of QuickCheck to Idris
Idris
57
star
3

IdrisAtGalois2015

Slides and exercises for the Idris course taught at Galois
Idris
50
star
4

epigram1

A version of Epigram 1 that can run with newer GHCs
Haskell
49
star
5

IdrisSqlite

Effectful bindings for SQLite (forked from IdrisWeb)
Idris
40
star
6

pudding-old

A language-integrated proof assistant, for and in Racket
Racket
40
star
7

final-pretty-printer

A monadic (and pretty) pretty printer for Haskell
Haskell
34
star
8

todo-list

A TODO list feature for DrRacket, like to Agda's goal list but for any language.
Racket
33
star
9

derive-all-the-instances

Work on type class deriving with elaboration reflection
Idris
31
star
10

idris-interaction.rkt

A Racket library for interacting with Idris over the IDE protocol
Racket
30
star
11

itu-thesis

A highly unofficial, still experimental LaTeX document class for ITU M.Sc. and Ph.D. theses and dissertations
TeX
20
star
12

tt-playground

A playground for type theory implementations in Racket
Racket
20
star
13

racket-zippers

A zipper library for Racket
Racket
19
star
14

dr-racket-like-unicode

A clone of DrRacket-style Unicode symbol input for Emacs
Emacs Lisp
17
star
15

dan-scheme

A very little language
Racket
15
star
16

idris-code-highlighter

A semantic highlighter for Idris code
Idris
14
star
17

idris-utils

Various Idris utility libraries. No guarantees. Some may end up in the stdlib someday, while others may be useless.
Idris
11
star
18

helm-idris

A Helm datasource for querying the Idris compiler
Emacs Lisp
10
star
19

tiny-dependent-types

A very simple implementation of a little dependently typed language
F#
10
star
20

prop-menu-el

Compute pop-up menus from text and overlay properties
Emacs Lisp
10
star
21

helm-pages

A Helm data source for pages in the current buffer
Emacs Lisp
10
star
22

bob24

Lean
10
star
23

jonprl-mode

An Emac major mode for writing JonPRL code
Emacs Lisp
8
star
24

pudding

Tactics in the macro expander
Racket
6
star
25

Brainfun

A Brainf**k interpreter in Idris
Idris
6
star
26

brush

A Racket literate programming system without tangling
Racket
6
star
27

annotated-wl-pprint

A variant of the Wadler-Leijen pretty-printer that allows arbitrary semantic annotations
Haskell
4
star
28

racket-presentation-gui

Prototype implementation of presentation-based UI widgets for Racket's GUI library
Racket
4
star
29

narrowed-page-navigation

An Emacs package for showing a buffer page-by-page, intended for presentations and live coding.
Emacs Lisp
4
star
30

ghc-imported-from-el

Emacs support for Carlo Hamalainen's ghc-imported-from
Emacs Lisp
4
star
31

helm-ghc

Helm support for ghc-mod metadata
Emacs Lisp
4
star
32

live-code-talks

An Emacs package to highlight special comments for in-buffer slide-shows.
Emacs Lisp
4
star
33

idris-tf-random

A port of the Haskell tf-random to Idris
C
3
star
34

barcodes-code128

A Haskell library for generating Code 128 barcodes
Haskell
3
star
35

scala-doc-search

A Hoogle clone for Scaladoc
Scala
3
star
36

iu-pict

A Racket pict for the IU logo
Racket
3
star
37

pretty-examples

Examples of our PP lib
Haskell
2
star
38

emacs-old-norse-input

An Old Norse input method for Emacs
Emacs Lisp
2
star
39

racket-abt

An ABT library for Racket
Racket
2
star
40

simple-relational-refinement

Haskell
1
star
41

typesearch

Scala
1
star
42

frank.el

Emacs mode for the Frank language
Emacs Lisp
1
star
43

idris-raytracer

Unfinished raytracer in Idris for use in testing compiler optimizations
1
star
44

dynamic-haskell-ffi

Experimentation with dynamically loading C libraries from Haskell (learning exercise)
Haskell
1
star
45

ssft24

Lean
1
star