typedefs / typedefs Goto Github PK
View Code? Open in Web Editor NEWProgramming language agnostic type construction language based on polynomials.
Home Page: http://typedefs.com/
License: GNU Affero General Public License v3.0
Programming language agnostic type construction language based on polynomials.
Home Page: http://typedefs.com/
License: GNU Affero General Public License v3.0
> 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
Moved into this issue from an older source code comment by @wires:
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)
We want to capture some of the documentation and learnings in source code comments, and generally present things as clearly as possible.
doc
targetTypedefs.idr
into issues or somethingIdris'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)
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.
TProd
and TSum
are currently binary constructors, but we want them to be n-ary.
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)
.
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.
default.nix
tparsec
dependency?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
Issue to collect related projects and write a Hashi-corp like "Typedefs v.s. $project"
List:
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
:
mu
is supposed to "chop off" the first variable - does that mean the one with a minimal index?(var 3)
(* (var 1) (var 0))
Working repository: https://github.com/typedefs/idris-gpd
The current name is confusing and clashes with Typedefs.showTDef
.
I've been busy with it lately and it's primarily motivated by future usage in typedefs.
As an initial syntax, we'll be going Lispwards.
Project management issue: typedefs/pm#1.
Moved into this issue from an older source code comment by @wires.
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
Run nix-shell
in the project dir containing default.nix.
From inside the shell, run:
idris --build typedefs.ipkg
Look at using Text.PrettyPrint.WL
to generate output. Possibly relevant to defining an interface, too.
The Nix build is great to have, but it's also problematic in areas. Maybe we'd want to timebox creating an Elba build?
Building using Nix is borked on my machine, so let's add another layer to make things 'easier'.
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
compile
button, and invoke the JS typedefs compiler on the textarea contentText.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 ASTtdefAst
is src/TParse.idr?).This is for tests, so we can add cases with Mu
. E.g. see #68
typedefs.ipkg
src
dirTypedefs
a proper module instead of a 'main' fileTest.
(should match dir and filenames)Examples.idr
src (should be main
module in the ipkg
)test
targetexamples
or run
targetWe 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:
Other suggestions welcomed.
Moved into this issue from an older source code comment by @wires:
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
@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.
The idea is that ParserJS.idr call the various Backends instead of just the Haskell one.
main
functionString
switch to select the desired backendThis is a probably somewhat outdated TODO:
showTDef
Backend.Haskell
: generate
, generateType
TermCodec
(serialize
and serializeMu
?)Re invocation of the Haskell backend, @clayrat writes
It's generally
generate <typedef>
orgenerateType <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).
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
?
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
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
Add some/all of the tests that we have for the parser, but for Backend.Haskell
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
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
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.
;
should be commentsA declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.