typedefs/typedefs

Programming language agnostic type construction language based on polynomials.

Typedefs

About

Typedefs is a programming language-agnostic, algebraic data type definition language, written in Idris.

See http://typedefs.com, or play around with examples at Try Typedefs!

Build and run

Nix package descriptions, an Elba manifest and a Makefile are provided.

Nix packages

If you want to build everything, do:

nix-build

If you only want to build a specific package:

nix-build -A typedefs.nix

Makefile

Build everything:

make build-lib
sudo make install-lib
make build-rest

Build a specific package:

make build pkg=typedefs

Build documentation:

make doc-all

Run tests:

make test-all

Install:

sudo make install-all

Clean up:

make clean-all

Elba

There is a complete tutorial on how to compile and install typedefs using the elba package manager here.

In most cases it should be just as easy as:

elba install

typedefs's Issues

Make binary TDef constructors n-ary

TProd and TSum are currently binary constructors, but we want them to be n-ary.

Create a parse test helper so we don't have to repeat the string to be parsed

We now have:

    it "\"(var 123)\"" $
      showTDef "(var 123)"
        `shouldBe` "Just (124 ** {123})"

We want something like:

    itShouldParseAs "(var 123)" "Just (124 ** {123})"

Actually, it would be nicer still if we could just construct a term t as the rhs, instead of the current showTDef t.

Maybe, while we're at it, for clarity, we should uppercase things in the tests from maybe, list, nil, cons, etc.

Remove old parsers

• rm old Text.Parse version in src/Parse.idr.
• tparseTDef in TParseTDef.idr is the one we actually want; that file whould be renamed.
• tparse currently parses to the old 'fake' non-dependently typed AST
  (tdefAst is src/TParse.idr?).

Tests for Haskell backend

Add some/all of the tests that we have for the parser, but for Backend.Haskell

JS API should expose top-level methods

Outline

The idea is that ParserJS.idr call the various Backends instead of just the Haskell one.

• expose Haskell backend
• expose ReasonML backend
• expose JSON backend
• expose type parser
• remove main function
• add a String switch to select the desired backend

Older version of this issue (plz update!)

This is a probably somewhat outdated TODO:

• expose showTDef
• expose Backend.Haskell: generate, generateType
• expose TermCodec (serialize and serializeMu?)

Re invocation of the Haskell backend, @clayrat writes

It's generally generate <typedef> or generateType <typedef>
depends on whether you're making type synonyms or actual new data
I'll try to add those tests later today

See #48.

Alex also mentioned idris-lang/Idris-dev#4073, which should allow us to create interfaces for Node (and, after some browserification, hopefully also for the browser).

Implement proto schema from js-stbx-packet-codec

https://github.com/statebox/js-stbx-packet-codec/blob/master/statebox.proto

Error reporting in TParsec

I've been busy with it lately and it's primarily motivated by future usage in typedefs.

Web UI groundwork

• compile the typedefs compiler to Javascript
• do so in a separate... Nix build file? or perhaps something a bit more workable
• create an HTML page with a textarea and a compile button, and invoke the JS typedefs compiler on the textarea content
• discuss further nicifications

Example types / terms for Bitcoin Wednesday demo

Add Show & Eq instances for Mu

This is for tests, so we can add cases with Mu. E.g. see #68

port Generic Packet Descriptions paper to Idris

Working repository: https://github.com/typedefs/idris-gpd

Nested types?

@kjekac brought up an example that doesn't seem to be expressible with current typedefs:

data Foobar a b = Foo | Bar a b (Foobar b a)

This is called "nested data types" in the literature, and there are ways to do it, e.g.:

http://pdfs.semanticscholar.org/7727/be5d8d65d9a76d544d352a17c4fe10a8d631.pdf Johann, Ghani, "Initial Algebra Semantics is Enough!"

Incorporating this would likely force us to redo typedefs as containers or something similar.

JS compilation via Nix fails when including Backend.Haskell in ParserJS.idr

Idris's JS compiler doesn't seem to like

import Typedef
import Parse
import Backend.Haskell

It complains about:

[nix-shell:/app/typedefs]# idris --build typedefs-parser-js.ipkg
Entering directory `./parser.js'
Type checking ./ParserJS.idr
Uncaught error: Elaborating {__infer_0} arg {ival_0}: NoSuchVariable run__IO
FAILURE: "idris-codegen-javascript" ["./ParserJS.ibc","-o","/app/typedefs/typedefs_parser.js"]
Leaving directory `./parser.js'

Removing the import Backend.Haskell makes the error go away and compilation succeed.

Update: this was using Nix 2.1.3 on macOS (pre-Mojave)

Non-Lispy grammar

Create type provider

Make unit test actually check stuff instead of just printing

We may want to keep it simple for now and write a few custom test functions, or we may want to look into one of these:

• https://github.com/jfdm/idris-testing
• https://github.com/pheymann/specdris

Other suggestions welcomed.

Rename Parse.showTDef to parseThenShowTDef

The current name is confusing and clashes with Typedefs.showTDef.

Automated build

• Create Travis 'project' for this repo (@wires)
• Do the Nix build thing

Add TermCodec tests

Codec for terms of type (Ty <-> Bits)

Moved into this issue from an older source code comment by @wires:

• discuss binary schema in upcoming meeting
• serialise : (t:Ty) -> x:(tau t) -> Bits
• deserialise : Bits -> (t:Ty ** tau t)

•   prf Term codec :
      forall t:Ty. forall (x:tau t). (deserialise . serialise) t x == t
  

nix-build fails on Travis with 'no such variable Vect'

Here's the Travis output: https://travis-ci.com/typedefs/typedefs/builds/89301620#L1051.

This issue is blocking @clayrat's very desirable term codec PR #68.

Try out idris-tparsec

Try switching the parsing library from Text.Parser to https://github.com/gallais/idris-tparsec/ to circumvent the laziness issues in #12

Paper: https://gallais.github.io/pdf/agdarsec18.pdf
Examples: https://github.com/gallais/idris-tparsec/tree/master/src/Examples

Elba build

The Nix build is great to have, but it's also problematic in areas. Maybe we'd want to timebox creating an Elba build?

Upgrade to Idris 1.2.0

Add Lisp-style line comment syntax

• Lines starting with ; should be comments

Application?

We probably want some internal notion of application if we want to be able to generate something like the following:

data List a = Nil | Cons a (List a)
data Nat = Z | S Nat
type ListNat = List Nat

One way would be to look at http://assert-false.net/arnaud/papers/A%20dissection%20of%20L.pdf, and have some degenerate form of it, e.g., where we only keep the contexts and never do actual substitution. This could also help with #61

Interpret type definitions (tau : Ty -> Type)

Moved into this issue from an older source code comment by @wires.

Use prettyprint

Look at using Text.PrettyPrint.WL to generate output. Possibly relevant to defining an interface, too.

whitespace parsing issues

> typedefs-parser '(var 0)'
Just (Var 0)
> typedefs-parser '(var 0) '
Nothing
> typedefs-parser '(mu list (cons (* (var 1) (var 0))) )'
Just (Mu "list" [(Prod (Var 1) (Var 0))])
> typedefs-parser '(mu list (cons (* (var 1) (var 0)) ))'
Nothing

Related projects

Issue to collect related projects and write a Hashi-corp like "Typedefs v.s. $project"

List:

• Universal Binary Format http://ubf.github.io/ubf/ubf-user-guide.en.html

Specify and implement a non-sexp typedefs grammar

It would be nice to have some semi-formal definition for how everything is defined. Most of it seems pretty evident, but there could be subtleties around var and mu:

• It has been mentioned that mu is supposed to "chop off" the first variable - does that mean the one with a minimal index?
• Do variable indexes always start from 0? This arises when trying to parse things from strings: e.g., do the following strings encode legit ASTs?

1. (var 3)
2. (* (var 1) (var 0))

Use 0,1 syntax instead of Void, Unit

Investigate/port the type matrices paper

https://github.com/byorgey/type-matrices
http://ozark.hendrix.edu/~yorgey/pub/type-matrices.pdf
http://ozark.hendrix.edu/~yorgey/pub/type-matrices-mpc-15.pdf

Create Docker image able to run the Nix build

Building using Nix is borked on my machine, so let's add another layer to make things 'easier'.

Document, clarify, clean up and format the main ADT and examples.

We want to capture some of the documentation and learnings in source code comments, and generally present things as clearly as possible.

• add doc comments to main types
• add doc comments to examples
• make sure the order of examples makes sense
• update makefile with an additional doc target
• move Jelle's todo list from the bottom of Typedefs.idr into issues or something

Parse into TDef data type

Up until now, the parser has been producing trees of an intermediate AST type. Instead, it should produce the Typedefs AST type TDefs, which can de done using a sigma type of the form (n : Nat ** TDef n).

nix-build fails due to incomplete definition of unpack

macOS 10.13.4
nix 2.1.3

Output:

➜  typedefs git:(master) nix-build default.nix -A typedefs
these derivations will be built:
  /nix/store/chwyrvnnh59ib11crq31d0nfr6qiqmkn-idris-typedefs-dev.drv
building '/nix/store/chwyrvnnh59ib11crq31d0nfr6qiqmkn-idris-typedefs-dev.drv'...
unpacking sources
unpacking source archive /nix/store/pqwi1h8976g6l8nab0hjnklywinl24w3-typedefs
source root is typedefs
patching sources
configuring
no configure script, doing nothing
building
Entering directory `./src'
Leaving directory `./src'
running tests
Entering directory `./src'
Type checking /private/tmp/nix-build-idris-typedefs-dev.drv-0/idris27013-0.idr
.idris-wrapped_: Erasure/getArity: definition not found for with block in Prelude.Strings.unpack
CallStack (from HasCallStack):
  error, called at src/Idris/Erasure.hs:602:20 in idris-1.3.0-HQONzYd57BmLbdAngG1p5r:Idris.Erasure
builder for '/nix/store/chwyrvnnh59ib11crq31d0nfr6qiqmkn-idris-typedefs-dev.drv' failed with exit code 1
error: build of '/nix/store/chwyrvnnh59ib11crq31d0nfr6qiqmkn-idris-typedefs-dev.drv' failed

Use Lisp-like parenthetical syntax

As an initial syntax, we'll be going Lispwards.

Project management issue: typedefs/pm#1.

Add Haskell type export to comand line parser

ReasonML codec

Codec for type definitions (Ty <-> Bits)

Moved into this issue from an older source code comment by @wires:

• define binary schema
• serialise : Ty -> Bits
• deserialise : Bits -> Ty

• prf Ty codec :
    forall t:Ty. (serialise . deserialise) t == t
  

Related snippet:

showTy x =
  case x of
    Ty0 => "0"
    Ty1 => "1"
    (a .+. b) => showOp "+" a b
    (a .*. b) => showOp "*" a b
  where
    parens : String -> String
    parens s = "(" ++ s ++ ")"
    showOp : String -> Ty -> Ty -> String
    showOp op x y = parens $ (showTy x) ++ " " ++ op ++ " " ++ (showTy y)

Doc comment on `data TDef` is rejected by the parser

https://github.com/typedefs/typedefs/blob/master/src/Typedefs.idr#L13

It says -- ||| now but it ought to be |||; not sure why this is happening, or if this still happens for Idris 1.3.

Add tests for parsing "(name ... ...)" into TName values

Use literate Idris

We want to turn turn the main .idr files into a literate Idris and turn it into a human readable article

Jelle sketched out some typedefs stuff here, please have a look and feel add comments

Compilation problem

Hey folks, nix-shell -A typedefs-parser-js gives me the following, any ideas where this comes from?

Type checking ./Parse.idr
Parse.idr:62:13:
   |
62 |     TMu nam $ weakenNTDefs xs (S m) (LTESucc prf)
   |             ^
When checking right hand side of weakenTDef with expected type
        TDef m

When checking an application of constructor Typedefs.TMu:
        Type mismatch between
                Vect k (Name, TDef m1) (Type of weakenNTDefs _ m _)
        and
                List (Name, TDef (S m)) (Expected type)

        Specifically:
                Type mismatch between
                        Vect k (String, TDef m1)
                and
                        List (String, TDef (S m))

Parse.idr:104:16-28:
    |
104 |        , map (\(nm, (n**td)) => (n ** TName nm td)) $
    |                ~~~~~~~~~~~~~
When checking right hand side of Parse.case block in tdef at Parse.idr:104:16-28 with expected type
        (n1 : Nat ** TDef n1)

When checking argument pf to constructor Builtins.MkDPair:
        No such variable TName

Let-bindings

We should probably introduce some aliasing/let binding syntax, so that we can define them in parts and referred back to, like in the ListNat test.

Syntax suggestions? Shall we introduce list literals (which i don't particularly like, but wth):

(let [ (name Maybe (+ 1 (var 0))
     , (mu ...)
     , ...
     ]
     (....tdef...)
)

Does this make any sense? :P I'm half-tempted to break sexp syntax where and go for a list of definitions like

foo = (+ 1 1)
bar = (...)

Actually, how should this interact with naming through TName and TMu?

Set up unit tests

• create typedefs.ipkg
• move sources into src dir
• make Typedefs a proper module instead of a 'main' file
• move tests into separate dir/file
• Prefix test modules with Test. (should match dir and filenames)
• move examples into an Examples.idr src (should be main module in the ipkg)
• update Makefile test target
• update Makefile with an additional examples or run target
• update Nix build

Nix 2.x build problems

Problem

The project will not build under Nix 2.x and Idris 1.2.0 using the build file default.nix. (NB: this is a branch.) Like Alex points out, this problem is described under NixOS/nixpkgs#33994.

The error:

Entering directory `./src'
 Can't find import Builtins
 Can't find import Prelude
 Can't find import Data/Fin

Reproduce

1. Run nix-shell in the project dir containing default.nix.

2. From inside the shell, run:

   idris --build typedefs.ipkg
   

Idris 1.3.0 build using Nix 2.0

• Fix compilation errors caused by the upgrade from 1.2.0 to 1.3.0
• Idris 1.3.0 builder for Nix 2.x
  • Is this available from somewhere?
  • If not, discuss feasibility, effort and value of doing this ourselves
• We probably want to do this in a dedicated build file independent of default.nix
• tparsec dependency?

Nix build failure

When I do nix-build on a clean clone of typedefs, the build fails as follows. Any ideas?

Entering directory `./src'
Type checking ./Types.idr
 Can't find import Token
builder for '/nix/store/wh1zhx12x8cz6bdsk3v5bwdbw2zvgcvn-idris-typedefs-dev.drv' failed with exit code 1
error: build of '/nix/store/jfmdyys1cwcq7vk0nhvzxzpa85a1adxc-idris-typedefs-examples-dev.drv', '/nix/store/wh1zhx12x8cz6bdsk3v5bwdbw2zvgcvn-idris-typedefs-dev.drv' failed