Coder Social home page Coder Social logo

gabriella439 / grace Goto Github PK

View Code? Open in Web Editor NEW
382.0 12.0 31.0 995 KB

A ready-to-fork interpreted functional language with type inference

License: BSD 3-Clause "New" or "Revised" License

Haskell 42.63% Nix 0.92% CSS 1.26% HTML 0.18% JavaScript 55.01%

grace's Introduction

grace

Grace (short for Fall-from-Grace) is a ready-to-fork implementation of a JSON-compatible functional programming language with type inference. You will most likely be interested in Grace for one of two reasons:

  • You need to implement a domain-specific language and you would like to begin from a quality existing implementation instead of embedding a syntax tree in JSON/YAML

  • You're interested in learning more about state-of-the-art algorithms for programming language theory by studying a clear and realistic reference implementation

If you're interested in code samples, then you can either jump down to the Quick tour section or check out the examples directory.

You can also try out Fall-from-Grace in your browser by visiting this page:

Build

You can build the grace executable using cabal:

$ cabal build exe:grace

Note: For older versions of cabal (e.g. version <3), use cabal new-build exe:grace. Known to work for at least cabal v.2.4

You can also build this project using Nix:

$ nix --extra-experimental-features 'nix-command flakes' build

… and you can build the live demo website for this project also using Nix:

$ nix --extra-experimental-features 'nix-command flakes' build .#website

You can also run grace without explicitly installing it:

$ nix --extra-experimental-features 'nix-command flakes' run github:Gabriella439/grace -- --help

Features

Grace implements the following features so that you don't have to:

  • Efficient and maintainable parsing

    Grace uses a lexer in conjunction with an Earley parser in order to improve the efficiency and predictability of parsing performance. In particular, the parser will run in linear time for any grammar accepted by an LR parser.

  • JSON-compatible syntax

    Grace uses the same syntax as JSON for records, lists, and scalar values, which means that many JSON expression are already valid Grace expressions:

    # This is valid Grace source code
    {
      "clients": [
        {
          "isActive": true,
          "age": 36,
          "name": "Dunlap Hubbard",
          "email": "[email protected]",
          "phone": "+1 (890) 543-2508"
        },
        {
          "isActive": true,
          "age": 24,
          "name": "Kirsten Sellers",
          "email": "[email protected]",
          "phone": "+1 (831) 564-2190"
        }
      ]
    }

    Don't like JSON syntax? No problem, the grammar is easy to change.

  • Bidirectional type-inference and type-checking

    Grace's type system is based on the Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism paper. This algorithm permits most types to be inferred without type annotations and the remaining types can be inferred with a single top-level type annotation.

  • JSON-compatible type system

    JSON permits all sorts of nonsense that would normally be rejected by typed languages, but Grace's type system is sufficiently advanced that most JSON expressions can be made valid with a type signature, like this:

    [ 1, [] ] : List (exists (a : Type) . a)

    … and this doesn't compromise the soundness of the type system.

  • Dhall-style imports

    You can import subexpressions by referencing their path or URL. You can also import JSON in the way same way since Grace is a superset of JSON.

  • Fast evaluation

    Grace implements normalization by evaluation to efficiently interpret code.

    The interpreter also doesn't need to warm up and has a low startup overhead of tens of milliseconds, so Grace is suitable for short-lived command-line tools.

  • Fixes to several JSON design mistakes

    The Grace interpreter supports comments, leading/trailing commas, and unquoted field names for input code while still emitting valid JSON output.

    This means that you can use Grace as a starting point for an ergonomic JSON preprocessor (similar to jsonnet, but with types).

  • Error messages with source locations

    Grace generates accurate and informative source locations in error messages, such as this:

    Not a subtype
    
    The following type:
    
      Bool
    
    (input):1:18: 
      │
    1 │ [ { x: 1 }, { x: true } ]
      │                  ↑
    
    … cannot be a subtype of:
    
      Natural
    
    (input):1:8: 
      │
    1 │ [ { x: 1 }, { x: true } ]
      │        ↑
    
  • Syntax highlighting and code formatting

    The interpreter highlights and auto-formats code, both for results and error messages. Note that the code formatter does not preserve comments (in order to simplify the implementation).

  • Open records and open unions

    Grace extends the bidirectional type-checking algorithm with support for inferring the types of open records (also known as row polymorphism) and open unions (also known as polymorphic variants). This lets you easily work with records or unions where not all fields or alternatives are known in advance.

  • Universal quantification and existential quantification

    Universal quantification lets you specify "generic" types (i.e. types parameterized on other types).

    Existential quantification lets you specify incomplete / partial types (i.e. types with holes that that the interpreter infers).

    Both universal and existential quantification work with types, open records, and open unions.

Also, the package and the code is extensively commented and documented to help you get started making changes. You can also read the CONTRIBUTING guide for instructions on how to get started.

Notable omissions

Grace does not support the following language features:

  • Input / output ("IO")

    Grace only supports pure computation and doesn't support an effect system for managing or sequencing effects

  • Type classes

    These require global coherence, which does not play nice with Dhall-style path-based imports

  • Type synonyms

    You cannot easily create short-hand synonyms for commonly used types

  • User-defined datatypes

    All data types in Grace are anonymous (e.g. anonymous records and anonymous unions), and there is no concept of a data declaration

  • Recursion or recursive data types

    Grace only supports two built-in recursive types, which are List and JSON, but does not support user-defined recursion or anonymous recursion.

  • String interpolation

    This is possible, but tricky, to lex, so I decided that it would be simpler to remove the feature.

Grace also does not support the following tooling:

  • A language server

    I will accept pull requests for this, but I don't plan on maintaining a language server myself since it's a lot of work and is a large surface area to maintain.

  • Code formatter that preserves comments

    I will probably reject pull requests to add this because I expect this would really clutter up the implementation and the concrete syntax tree.

  • Extensive documentation

    Grace is not really meant to be used directly, but is instead intended to be forked and used as a starting point for your own language, so any documentation written for Grace would need to be substantially rewritten as you adjust the language to your needs.

    That said, this README has a brief tour of the language below.

    If you still need an example of a tutorial for a similar language that you can adapt, see the Dhall language tour.

Development

You can get started on changing the language to your liking by reading the CONTRIBUTING guide.

If you're interested in upstreaming your changes, then these are the issues and pull requests I'm most likely to accept:

  • Bug fixes

  • Improving error messages

  • Fixes to build against the latest version of GHC or dependencies

  • Adding new built-ins

    … especially if they are likely to be widely used by downstream implementations.

  • Adding features with a high power-to-weight ratio

    Basically, anything that isn't too complicated and likely to be generally useful is fair game, especially if it's easy for forks to delete or disable if they don't want it.

  • Simpler and clearer ways of implementing existing functionality

    For example, if you think there's a way to simplify the type-checker, parser, or evaluator without too much regression in functionality then I'll probably accept it.

  • Adding more comments or clearer contributing instructions

    … so that people can more easily adapt the language to their own use case.

  • Syntactic sugar

    For example, I'd probably accept pull requests to compress the syntax for nested foralls or nested lambdas.

These are the issues and pull requests that I'm most likely to reject:

  • Anything that significantly increases my maintenance burden

    This project is more of an educational resource, like an executable blog post, than a production-ready package. So I commit to maintaining to this about as much as I commit to maintaining a blog post (which is to say: not much at all, other than to merge or reject pull requests).

  • Anything that significantly deteriorates the clarity of the code

    It's far more important to me that this code is pedagogically useful than the code being production-ready. Again, think of this project as an executable tutorial that people can learn from.

  • Any request to publish binaries or official releases

    This project is made to be forked, not directly used. If you want to publish anything, then fork the project and maintain binaries/releases yourself.

Acknowledgments

Your fork doesn't need to credit me or this project, beyond what the BSD 3-clause license requires. The only thanks I need is for people to use Grace instead of creating yet another domain-specific language embedded in JSON or YAML.

Quick tour

This section provides a lightning tour that covers all language features as briefly as possible, directed at people who already have some experience with typed and functional programming languages.

Command line

This package builds a grace executable with the following command-line API:

$ grace --help
Usage: grace COMMAND
  Command-line utility for the Grace language

Available options:
  -h,--help                Show this help text

Available commands:
  interpret                Interpret a Grace file
  text                     Render a Grace text literal
  format                   Format Grace code
  builtins                 List all built-in functions and their types
  repl                     Enter a REPL for Grace

You can use the interpret subcommand for interpreting a single file:

# ./example.ffg
let greet = \name -> "Hello, " + name + "!"

in  greet "world"
$ grace interpret example.ffg
"Hello, world!"

… and you can specify - to process standard input instead of a file, like this:

$ grace interpret - <<< '2 + 2'
4

You can also use the repl subcommand for interactive usage:

$ grace repl
>>> :let x = 1
>>> :let y = 2
>>> x + y
3

Data

Grace supports the following Scalar types:

  • Bools, such as false and true

  • Natural numbers, such as 0, 1, 2, …

  • Integers, such as -2, -1, 0, 1, 2, …

    Natural numbers are a subtype of Integers

  • Reals, such as 3.14159265, 6.0221409e+23, …

    Integers are a subtype of Reals

  • Text, such as "", "Hello!", "ABC", …

    Text supports JSON-style escape sequences

… and the following complex data structures:

  • Lists, such as [], [ 2, 3, 5 ], …

  • Optional types, such as null

    There is no special syntax for a present Optional value. Every type T is a subtype of Optional T. For example:

    [ 1, null ] : List (Optional Natural)
  • Records, such as {}, { x: 2.9, y: -1.4 }

    Record field names usually don't need to be quoted unless they require special characters

  • Unions, such as Left 1, Right True

    Any identifer beginning with an uppercase character is a union tag. You don't need to specify the type of the union, since union types are open and inferred.

  • JSON, such as [ 1, [ true, "" ] ]

    … which is a supertype of all expressions that are also valid JSON.

Note that unions are the only data structure that is not JSON-compatible, since JSON does not support unions.

You can nest complex data structures arbitrarily, such as this example list of package dependencies:

[ GitHub
    { repository: "https://github.com/Gabriel439/Haskell-Turtle-Library.git"
    , revision: "ae5edf227b515b34c1cb6c89d9c58ea0eece12d5"
    }
, Local { path: "~/proj/optparse-applicative" }
, Local { path: "~/proj/discrimination" }
, Hackage { package: "lens", version: "4.15.4" }
, GitHub
    { repository: "https://github.com/haskell/text.git"
    , revision: "ccbfabedea1cf5b38ff19f37549feaf01225e537"
    }
, Local { path: "~/proj/servant-swagger" }
, Hackage { package: "aeson", version: "1.2.3.0" }
]

Types and annotations

You can annotate a value with type using the : operator. The left argument to the operator is a value and the right argument is the expected type:

  true : Bool
# ↑      ↑
# Value  Expected type

You can also ask to include the inferred type of an interpreted expression as a type annotation using the --annotate flag:

$ grace interpret --annotate - <<< '[ 2, 3, 5 ]'
[ 2, 3, 5 ] : List Natural

Here are some example values annotated with types::

true : Bool

"Hello" : Text

1 : Natural

1 : Integer  # `Natural` numbers also type-check as `Integer`s

1 : Real     # All numbers type-check as `Real`s

1 : Optional Natural  # Everything type-checks as `Optional`, too

[ true, false ] : List Bool

[ ] : forall (a : Type) . List a

{ name: "John", age: 24 } : { name: Text, age: Natural }

Left 1 : forall (a : Alternatives) . < Left: Natural | a >

[ Left 1, Right true ]
  : forall (a : Alternatives) . List < Left: Natural | Right: Bool | a >

Integer/even : Integer -> Bool

[ 1, true ] : JSON  # Any expression that is valid JSON type-checks as `JSON`

Control

Grace supports some operators out-of-the-box, such as:

  • Addition: 2 + 3
  • Multiplication: 2 * 3
  • Logical conjunction: true && false
  • Logical disjunction: true || false
  • Text concatenation: "AB" + "CD"
  • List concatenation: [ 2, 3 ] + [ 5, 7 ]

You can also consume boolean values using if / then / else expressions:

$ grace interpret - <<< 'if true then 0 else 1'
0

You can define immutable and lexically-scoped variables using the let and in keywords:

let name = "redis"

let version = "6.0.14"

in  name + "-" + version

You can access record fields using .:

let record = { turn: 1, health: 100 }

in  record.turn

You can pattern match on a union using the merge keyword by providing a record of handlers (one per alternative):

let render
      : < Left: Real | Right: Bool > -> Text
      = merge
          { Left: Real/show
          , Right: \b -> if b then "true" else "false"
          }

in  [ render (Left 2.0), render (Right true) ]

There is no way to consume Optional values (not even using merge). The Optional type solely exists for compatibility with JSON (so that null is not rejected). If you actually want a usable Optional type then use a union with constructors named Some or None (or whatever names you prefer):

let values = [ Some 1, None { } ]

let toNumber = merge { Some: \n -> n, None: \_ -> 0 }

in  List/map toNumber values

If you don't care about JSON compatibility then you can edit the language to remove null and Optional.

Grace supports anonymous functions using \input -> output syntax. For example:

let twice = \x -> [ x, x ]

in  twice 2

You can also use the built-in functions, including:

# Compare two `Reals` for equality
Real/equal : Real -> Real -> Bool

# Check if one `Real` is less than another `Real`
Real/lessThan : Real -> Real -> Bool

# Negate a `Real` number
Real/negate : Real -> Real

# Render a `Real` number as `Text`
Real/show : Real -> Text

# Drop the first N elements from a `List`
List/drop : forall (a : Type) . Natural -> List a -> List a

# Compare two lists for equality, given an element-wise equality test
List/equal : forall (a : Type) . (a -> a -> Bool) -> List a -> List a -> Bool

# Fold a list
List/fold
  : forall (a : Type) .
    forall (b : Type) .
      { cons: a -> b -> b, nil: b } -> List a -> b

# Get the first element of a list
List/head
  : forall (a : Type) .
    forall (b : Alternatives) .
      List a -> < Some: a | None: { } | b >

# Annotate each element of a list with its index
List/indexed : forall (a : Type) . List a -> List { index: Natural, value: a }

# Get the last element of a list
List/last
  : forall (a : Type) .
    forall (b : Alternatives) .
      List a -> < Some: a | None: { } | b >

# Compute the length of a list
List/length : forall (a : Type) . List a -> Natural

# Transform each element of a list
List/map : forall (a : Type) . forall (b : Type) . (a -> b) -> List a -> List b

# Reverse a list
List/reverse : forall (a : Type) . List a -> List a

# Take the first N elements of a list
List/take : forall (a : Type) . Natural -> List a -> List a

# Returns `true` if the `Integer` is even
Integer/even : Integer -> Bool

# Negate an `Integer`
Integer/negate : Integer -> Integer

# Returns `true` if the `Integer` is false
Integer/odd : Integer -> Bool

# Compute the absolute value of an `Integer`
Integer/abs : Integer -> Natural

# Fold a JSON value
JSON/fold
  : forall (a : Type) .
      { array: List a -> a
      , bool: Bool -> a
      , real: Real -> a
      , integer: Integer -> a
      , natural: Natural -> a
      , "null": a
      , object: List { key: Text, value: a } -> a
      , string: Text -> a
      } ->
      JSON ->
        a

# Fold a `Natural` number
Natural/fold : forall (a : Type) . Natural -> (a -> a) -> a -> a

# Compare two `Text` values for equality
Text/equal : Text -> Text -> Bool

For an up-to-date list of builtin functions and their types, run the grace builtins subcommand.

Type checking and inference

By default, the type-checker will infer a polymorphic type for a function if you haven't yet used the function:

$ grace interpret --annotate - <<< '\x -> [ x, x ]'
(\x -> [ x, x ]) : forall (a : Type) . a -> List a

However, if you use the function at least once then the type-checker will infer a monomorphic type by default, so code like the following:

let twice = \x -> [ x, x ]

in  twice (twice 2)

… will be rejected with a type error like this:

Not a subtype

The following type:

   List Natural

./example.ffg:1:19: 
  │
1 │ let twice = \x -> [ x, x ]
  │                   ↑

… cannot be a subtype of:

   Natural

./example.ffg:1:14: 
  │
1 │ let twice = \x -> [ x, x ]
  │              ↑

… because the inner use of twice thinks x should be a Natural and the outer use of twice thinks x shoud be a List Natural.

However, you can fix this by adding a type signature to make the universal quantification explicit:

let twice : forall (a : Type) . a -> List a         
          = \x -> [ x, x ]

in  twice (twice 2)

… and then the example type-checks. You can read that type as saying that the twice function works forall possible Types that we could assign to a (including both Natural and List Natural)..

You can also use existential quantification for parts of the type signature that you wish to omit:

let numbers : exists (a : Type) . List a
            = [ 2, 3, 5 ]

in  numbers

The type-checker will accept the above example and infer that the type a should be Natural for each element. You can read that type as saying that there exists a Type that we could assign to a that would make the type work, but we don't care which one.

You don't need type annotations when the types of values exactly match, but you do require type annotations to unify types when one type is a proper subtype of another type.

For example, Natural and Integer are technically two separate types, so if you stick both a positive and negative literal in a List then type-checking will fail:

$ grace interpret - <<< '[ 3, -2 ]'
Not a subtype

The following type:

   Integer

(input):1:7: 
  │
1 │ [ 3, -2 ]
  │       ↑

… cannot be a subtype of:

   Natural

(input):1:3: 
  │
1 │ [ 3, -2 ]
  │   ↑

… but if you add an explicit type annotation then type-checking will succeed:

$ grace interpret - <<< '[ 3, -2 ] : List Integer'
[ 3, -2 ]

There is one type that is a supertype of all types, which is exists (a : Type) . a (sometimes denoted in the literature), so you can always unify two disparate types, no matter how different, by giving them that type annotation:

$ grace interpret - <<< '[ { }, \x -> x ] : List (exists (a : Type) . a)'
[ { }, \x -> x ]

Note that if you existentially quantify a value's type then you can't do anything meaningful with that value; it is now a black box as far as the language is concerned.

Open records and unions

The interpreter can infer polymorphic types for open records, too. For example:

$ grace interpret --annotate - <<< '\x -> x.foo'
(\x -> x.foo) : forall (a : Type) . forall (b : Fields) . { foo: a, b } -> a

You can read that type as saying that \x -> x.foo is a function from a record with a field named foo to the value of that field. The function type also indicates that the function works no matter what type of value is present within the foo field and also works no matter what other fields might be present within the record x.

You can also use existential quantification to unify records with mismatched sets of fields. For example, the following list won't type-check without a type annotation because the fields don't match:

$ grace interpret - <<< '[ { x: 1, y: true }, { x: 2, z: "" } ]'
Record type mismatch

The following record type:

   { z: Text }

(input):1:22: 
  │
1 │ [ { x: 1, y: true }, { x: 2, z: "" } ]
  │                      ↑

… is not a subtype of the following record type:

   { y: Bool }

(input):1:3: 
  │
1 │ [ { x: 1, y: true }, { x: 2, z: "" } ]
  │   ↑

The former record has the following extra fields:

• z

… while the latter record has the following extra fields:

• y

… but if we're only interested in the field named x then we can use a type annotation to tell the type-checker to ignore all of the other fields by existentially quantifying them:

[ { x: 1, y: true }, { x: 2, z: "" } ]
    : List (exists (a : Fields) . { x: Natural, a })

We can still write a function that consumes this list so long as the function only accesses the field named x:

let values
      : exists (a : Fields) . List { x: Natural, a }
      =  [ { x: 1, y: true }, { x: 2, z: "" } ]

in  List/map (\record -> record.x) values

The compiler also infers universally quantified types for union alternatives, too. For example:

$ grace interpret --annotate - <<< '[ Left 1, Right true ]'
[ Left 1, Right true ]
  : forall (a : Alternatives) . List < Left: Natural | Right: Bool | a >

The type is universally quantified over the extra union alternatives, meaning that the union is "open" and we can keep adding new alternatives. We don't need to specify the desired type or set of alternatives in advance.

JSON

You can make all sorts of weird expressions type-check by adding a type annotation of JSON:

[ true, 1, [ -2, false, "" ], null, { foo: { } } ] : JSON

… but the only way you can consume an expression of type JSON is to use JSON/fold, which has the following type:

JSON/fold
  : forall (a : Type) .
      { array: List a -> a
      , bool: Bool -> a
      , real: Real -> a
      , integer: Integer -> a
      , natural: Natural -> a
      , "null": a
      , object: List { key: Text, value: a } -> a
      , string: Text -> a
      } ->
      JSON ->
        a

This is similar in spirit to a merge expression where you need to specify how to handle every possible case that the JSON value could possibly be.

For example, the following expression

JSON/fold
  { "bool": \b -> if b then 1 else 0
  , "natural": \x -> x
  , "integer": Integer/abs
  , "real": \_ -> 1
  , "string": \_ -> 2
  , "null": 3
  , "object": List/length
  , "array": List/fold { nil: 0, cons: \x -> \y -> x + y : Natural }
  }
  [ true, 1, [ -2, false, "" ], null, { foo: { } } ]

… evaluates to 10.

There is no other way to consume a JSON value other than to specify how to handle every single case, because once you annotate a value as having type JSON then the interpreter can no longer guarantee that the value is a List, record, or a specific scalar value. This is why you should prefer to use a more precise type annotation if possible and only use JSON as a type annotation as a last resort.

Imports

Grace has two ways to import expressions from other sources: Filepath-based imports and imports using URIs.

Imports from files

You can import a Grace subexpression stored within a separate file by referencing the file's relative or absolute path.

For example, instead of having one large expression like this:

[ { name: "Cake donut"
  , batters: [ "Regular", "Chocolate", "Blueberry", "Devil's Food" ]
  , topping: [ "None"
             , "Glazed"
             , "Sugar"
             , "Powdered Sugar"
             , "Chocolate with Sprinkles"
             , "Chocolate"
             , "Maple"
             ]
  }
, { name: "Raised donut"
  , batters: [ "Regular" ]
  , topping: [ "None", "Glazed", "Sugar", "Chocolate", "Maple" ]
  }
, { name: "Old Fashioned donut"
  , batters: [ "Regular", "Chocolate" ]
  , topping: [ "None", "Glazed", "Chocolate", "Maple" ]
  }
]

… you can split the expression into smaller files:

# ./cake.ffg

{ name: "Cake donut"
, batters: [ "Regular", "Chocolate", "Blueberry", "Devil's Food" ]
, topping: [ "None"
           , "Glazed"
           , "Sugar"
           , "Powdered Sugar"
           , "Chocolate with Sprinkles"
           , "Chocolate"
           , "Maple"
           ]
}
# ./raised.ffg

{ name: "Raised donut"
, batters: [ "Regular" ]
, topping: [ "None", "Glazed", "Sugar", "Chocolate", "Maple" ]
}
# ./old-fashioned.ffg

{ name: "Old Fashioned donut"
, batters: [ "Regular", "Chocolate" ]
, topping: [ "None", "Glazed", "Chocolate", "Maple" ]
}

… and then reference them within a larger file, like this:

[ ./cake.ffg
, ./raised.ffg
, ./old-fashioned.ffg
]

You can also import functions in this way, too. For example:

# ./greet.ffg

\name -> "Hello, " + name + "!"
$ grace interpret - <<< './greet.ffg "John"'
"Hello, John!"

Any subexpression can be imported in this way.

Imports using URIs

Imports with URIs work similar to the ones using a simple filepath.

Suppose you do not have the greet.ffg stored locally but instead it resides on a web server: http://example.com/grace/greet.ffg You could either download it and reference it by its filepath like demonstrated in the example above or let the Grace interpreter do the job:

$ grace interpret - <<< 'http://example.com/grace/greet.ffg "John"'
"Hello, John!"

Grace supports the following URI schemes:

  • HTTP: https://… or http://…

    $ grace interpret - <<< 'https://raw.githubusercontent.com/Gabriel439/grace/5b3c0e11ee4776a42c26c1986bef8a17dd329e2e/prelude/bool/not.ffg true'
    false
  • Files: file:…

    $ grace interpret - <<< 'file:/path/to/greet.ffg "John"'
    "Hello, John!"
  • Environment variables: env:…

    $ MY_VAR='"Hello !"' grace interpret - <<< 'env:MY_VAR'
    "Hello !"

Prelude

You can import a small standard library of utilities from the following URL:

These utilities provide higher-level functionality that wraps the underlying builtins.

Here is an example of how to use the Prelude:

let prelude =
      https://raw.githubusercontent.com/Gabriel439/grace/main/prelude/package.ffg

in  prelude.bool.not true

The Prelude is organized as a large and nested record that you can import. Each sub-package of the Prelude is a top-level field, and the utilities are nested fields within each sub-package.

You can also directly import the utility you need, which is faster since it only requires a single HTTP request:

let not =
      https://raw.githubusercontent.com/Gabriel439/grace/main/prelude/bool/not.ffg

in  not true

Name

Like all of my programming language projects, Grace is named after a character from PlaneScape: Torment, specifically Fall-from-Grace, because Grace is about slaking the intellectual lust of people interested in programming language theory.

The name of this interpreter conflicts with another programming language, so use the longer name, "Fall-from-Grace", to disambiguate when it's not clear from the context. Either way, you'll want to rename this project when you fork it.

grace's People

Contributors

bts avatar crazypython avatar debugsteven avatar erjenkins29 avatar evanrelf avatar fishtreesugar avatar gabriella439 avatar gardspirito avatar imalsogreg avatar mlang avatar mmhat avatar mr-andersen avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

grace's Issues

Nix build fails at `remote-import` test

Thanks for this project!

On current main (ce01be3), I'm seeing that nix build fails while running the tasty test suite. Looking at the logs, the failure appears to be

remote-import-input - error:                            FAIL
          Missing golden value.

(expected behavior: pass, or possibly skip this test when building with Nix?)

Annotating subexpressions

Hey, firstly just wanted to thank you for this resource - it's been very useful!

I'd like to desugar my language into something like GHC's Core, which means I need to be able to annotate subexpressions with types. This algorithm doesn't seem to support that out of the box, and the adjustments I've poorly made haven't worked very well.
Do you know if this is possible / practical to do? Any pointers as to how I could do this?

Thanks a lot!

Union `subtype` Union: p0 == p1 not handled?

grace/src/Grace/Infer.hs

Lines 667 to 669 in cd70563

case p0First <|> p1First of
Nothing -> do
throwError (MissingOneOfAlternatives [Type.location _A0, Type.location _B0] p0 p1 _Γ)

— here, it's assumed that either p0 is first and p1 follows it or p1 is first and p0 follows it.
The case where p0 is p1 is not handled.

Does it always have to be true?
(Asking because I ran into Internal error)

Relation to Dhall

Since you are the creator of Dhall I wonder how this project of yours relates to that? As far as I can tell both projects have similar goal although Grace is a bit more restricted (i.e. primarily targeting JSON) and no remote imports but Text equality - at least that is what I have discovered so far.
The questions that came to my mind are: Is it a playground to try out new things for Dhall? Will the projects merge eventually? Or is it a study for its own sake? Basically: What was the motivation for Grace?
I guess a section in the README would be nice.

That being said, I am really excited about this project! Thank you for sharing it! 🚀

Confusing claim on parsing performance

The README says: “Grace uses a lexer in conjunction with an LR parsing package”. But I looked at the sources and it’s using Earley, which is not LR.

Further, the README also claims “you can easily extend or amend Grace's grammar without taking special precautions to avoid performance pitfalls”, but worst-case time complexity for an Earley parser is cubic, so that doesn’t seem true either.

Perhaps you initially used happy or some other LR parser generator where those claims were true? Should the README be updated?

Use Scientific instead of Double

Since Integer is a subtype of Double and the former one is unbounded while the latter one is not we may run into troubles if we were upcasting a large number. Thus we may consider to use only machine types or use unbounded numeric types all over the place.

Personally I am totally fine if we use Int/Double since those have better performance characteristics and I do not expect to encounter such large numbers anyway. I still think it was nice if we are consistent in our implementation.

Arithmetic operator fixity is unintuitive

>>> 1 + 2 * 3
9

>>> 1 + (2 * 3)
7

Grace isn't giving * a higher fixity than +.

This originates in the parser:

ghci> parse "test" "1 + 2 * 3"
Right (Operator
  { location = 0,
    left = Operator
        { location = 0,
          left = Scalar {location = 0, scalar = Natural 1},
          operatorLocation = 2,
          operator = Plus,
          right = Scalar {location = 4, scalar = Natural 2}
        },
    operatorLocation = 6,
    operator = Times,
    right = Scalar {location = 8, scalar = Natural 3}
  })

Plus and times aren't robust for beta reduction

The subtyping and ad-hoc type of + make it a bit flaky.

This works fine:

>>> (\x -> 3.4 + x) 1
4.4

But this one doesn't

>>> 3.4 + 1
Not a subtype
The following type:
  Real
 cannot be a subtype of:
  Natural

All I've done here is beta reduction, which one would usually expect to preserve type inference.

Ideally, I think this should also work:

>>> (\x -> 1 + x) 3.14
Not a subtype

I can see why is doesn't, but Ignoring that + also does lists and text.

>>> :t (\x -> 1 + x)
Natural -> Natural

Could it instead be something like:

>>> :t (\x -> 1 + x)
forall (a : Type) such that (Natural <: a). a -> a

Structured exceptions

While text-based errors are okay if were just developing Grace as an standalone CLI interpreter the demands are somewhat different if we are using Grace as a library. Consider the following usecase:
We are building some kind of web application that consumes Grace code. During that process the integrated Grace interpreter throws an exception (E.g. an upload does not type check.) and we want to display that exception in an HTML document. Ideally we want to link to the location of the error.
But since all error output is text it is hard to extract the location - we must parse the error message to obtain that information.

Therefore we should consider using a more structured approach to exceptions and leave the rendering to the consumer.

Remote imports

Since there are Dhall-style file imports, are there any plans to add remote imports as well?

Question about subtyping

Hello, I'm studying Grace and curious about the way it handles type inference with subtyping.

So consider this case which TYPES ok:

; cabal run -- grace interpret --annotate - <<< '[{answer: null}, {answer: 42}]'
[ { "answer": null }, { "answer": 42 } ] : List { answer: Optional Natural }

and this which FAILS:

; cabal run -- grace interpret --annotate - <<< '[{answer: 42}, {answer: null}]'
Not a subtype
...

So the depending on the order of elements in the list it either succeeds or fails which can be then fixed (suggested by the README) by adding a type annotation with an existential List ?:

; cabal run -- grace interpret --annotate - <<< '[{answer: 42}, {answer: null}] : List ?'
[ { "answer": 42 }, { "answer": null } ] : List ?

I think this can be a bit confusing to users (that in those two similar cases they either required or not to add type annotations). Do you think it's worth fixing and/or possible to fix by synthesising List ? type for List constructor?

Unicode parsing issues

$ cat kaomoji.ffg 
{"hi": "(^▽^)"}
$ grace interpret kaomoji.ffg
grace: kaomoji.ffg: hGetContents: invalid argument (invalid byte sequence)

This is valid JSON and valid UTF-8

exists (a : Type). a <: forall (a : Type). a

I was trying to introduce impredicative instantiation for my fork of FFG. I thought that it's easy to do, given η-law is sacrificed, if I just expand <:∀R and <:∃L cases of subtype (correct me if I'm wrong). While I was doing that, I suddenly realized that subtype handles Forall and Exists in an exactly same manner.

So I built 7f63aa8 and, surprise-surprise, something is definitely off with this approach:
EDIT: There's something strange with Exists, subtype check. I tested relatively old commit 7f63aa8, and here's what I've got:

let test
    : exists (a : Type). a
	= 3
in test : forall (a : Type). a
❯ nix shell github:Gabriella439/grace/7f63aa8a1835ca1a782f18eb773c80ea2af4cd5f

❯ grace interpret test.ffg --annotate
3 : forall (a : Type) . a

unable to build executable in wsl2 ubuntu-20.04

Hello -- trying to simply build the executable, but running into the below issue.

Environment

  • windows wsl 2 (ubuntu-20.04)
  • ghc 8.6.2
  • cabal-install 2.4.0.0

steps to recreate

  1. in wsl environment, clone the repo
  2. sudo apt-get install cabal-install zlib1g-dev,
  3. cabal new-build exe:grace

(NOTE: cabal build fails at resolving any of the dependencies, so was forced to use cabal new-build)

expected outcome

build succeeds and grace command is compiled

actual outcome

fails with the following traceback:

$ cabal new-build exe:grace
Build profile: -w ghc-8.6.5 -O1
In order, the following will be built (use -v for more details):
 - grace-1.0.0 (lib) (first run)
 - grace-1.0.0 (exe:grace) (first run)
Preprocessing library for grace-1.0.0..
Building library for grace-1.0.0..
[ 9 of 21] Compiling Grace.Monotype   ( src/Grace/Monotype.hs, /home/evan/grace/dist-newstyle/build/x86_64-linux/ghc-8.6.5/grace-1.0.0/build/Grace/Monotype.o )

src/Grace/Monotype.hs:103:34: error:
    • No instance for (Lift Text)
        arising from the first field of ‘VariableFields’ (type ‘Text’)
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (Lift RemainingFields)
    |
103 |     deriving stock (Eq, Generic, Lift, Show)
    |                                  ^^^^

src/Grace/Monotype.hs:120:34: error:
    • No instance for (Lift Text)
        arising from the first field of ‘VariableAlternatives’
          (type ‘Text’)
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (Lift RemainingAlternatives)
    |
120 |     deriving stock (Eq, Generic, Lift, Show)
    |                                  ^^^^
cabal: Failed to build grace-1.0.0 (which is required by exe:grace from
grace-1.0.0).```

[Q] Impredicativity issues while checking that record is a subtype of a record?

Sorry for the title, I'm far from being great at type theory, but generally here's the issue:

# Works just fine!
let wrappedId
  : { wrapped : forall (a: Type). a -> a } 
  = { wrapped : \x -> x }
in wrappedId
❯ grace interpret example.ffg --annotate
{ "wrapped": \x -> x } : { wrapped: forall (a : Type) . a -> a }

But then, if we add type annotation at the end:

let wrappedId
  : { wrapped : forall (a: Type). a -> a } 
  = { wrapped : \x -> x }
in wrappedId : { wrapped: forall (a : Type) . a -> a }
❯ grace interpret example.ffg --annotate
Unbound type variable: a

example.ffg:4:47: 
  │
4 │ in wrappedId : { wrapped: forall (a : Type) . a -> a }
  │                                               ↑

This type annotation, though:

in wrappedId : forall (a : Type). { wrapped: a -> a }

does the job.

Builtin Map type

When working with Dhall every now and then I with for something that is a record, but with a fixed type for all the fields. Records have the advantage that we can address fields by name (record_value.field_name) but we cannot talk about the types of the fields. Lists have the advantage that we can do this - for instance, we can map over the elements - but we cannot address an element in a type-safe way. The idea is to have something combining both, i.e. a homogenous record. But it might be better to call it a Map (or an Object or a Dictionary). Since we have subtyping in this language this type would probably a subtype of Record and can be easily converted to a List.

A first idea for the syntax: {! field1 : value1, field2 : value1, ... }, i.e. the only difference is the exclamation mark after the opening brace (no whitespace allowed inbetween - it parses as one token). This has the disadvantage that it might be easily confused with a record when one is skimming through some source code but on the other hand it one can quickly change a Record type to a Map type.

JSON/fold example in the README doesn't work

Hi there 👋

When I attempt to paste the following snippet from the README into the Grace browser:

JSON/fold
  { "bool": \b -> if b then 1 else 0
  , "natural": \x -> x
  , "integer": Integer/abs
  , "real": \_ -> 1
  , "string": \_ -> 2
  , "null": 3
  , "object": List/length
  , "array": \vs -> List/fold vs (\x -> \y -> x + y : Natural) 0
  }
  [ true, 1, [ -2, false, "" ], null, { foo: { } } ]

I get:


 Not a subtype

The following type:

  List a?

(input):1:1: 
  │
1 │ JSON/fold
  │ ↑

… cannot be a subtype of:

  { cons: b? -> c? -> c?, nil: c? }

(input):9:21: 
  │
9 │   , "array": \vs -> List/fold vs (\x -> \y -> x + y : Natural) 0
  │                     ↑

I can't understand how I might fix this given that Grace doesn't support recursion, which seems like it'd be necessary in order to get the result that the README suggests: 10. In fact I'm having trouble understanding the usefulness of JSON/fold at all given that recursion isn't supported...

Error when interpreting `examples/reddit-haskell.ffg`

Everything here was run from 4d32d09. I get this error when trying to run the Reddit r/haskell example:

λ grace interpret examples/reddit-haskell.ffg
Unbound fields variable: b

examples/reddit-haskell.ffg:6:23:

6 │               { data: { children: List
  │                       ↑

I fiddled with this for quite a while, trying to narrow down what's going wrong. Here's a more minimal reproducing case which produces the same error:

λ cat bad.ffg
let bad = { a: 42 } : exists (etc : Fields) . { a: Natural, etc }

in  bad.a
λ grace interpret bad.ffg
Unbound fields variable: etc

bad.ffg:1:47:

1 │ let bad = { a: 42 } : exists (etc : Fields) . { a: Natural, etc }
  │                                                 ↑

When I stop trying to get the a field, and just get the whole thing back, it works:

 let bad = { a: 42 } : exists (etc : Fields) . { a: Natural, etc }

-in  bad.a
+in  bad
λ grace interpret bad.ffg
{ "a":
    42
}

Advice for implementing type aliases

I have forked grace to use as a language for specifying biologically realistic neural networks, and I would like to provide the user with a few (hard-coded) type aliases, like:

  • Neuron ~ { segments: List Segment, membranes: List Membrane }
  • Membrane ~ List { channel: Channel, channel_conductance: Real }
  • Channel ~ { activation: Optional Gating, inactivation: Optional Gating, gates: Natural }
  • TimeConstant ~ < Instantaneous | Exponential { tau: Real } | Linear { slope: Real, offset: Real } >

My ideal type aliases have a similar role to Haskell's newtypes: they constrain the type of the value they contain, in addition to just providing a syntactic shorthand. And any value that satisfies the right-hand-side should ideally be inferred to have the type on the left-hand side.

I'm a bit stuck in the design:

  • I might add new values to Syntax.Scalar, making a concrete Neuron, Segment, Membrane scalar type, and then have the infer function return these directly if inference encounters the compatible record or alternative.
  • Or maybe there should be a new Type called Alias { name :: Text, type_ :: Type s }, and resolving type aliases should be done abstractly.

Do you have thoughts about these? Or is it known that type aliases are just incompatible with grace's bidirectional type checking for some reason?

Thanks! And please feel free to close this issue as off-topic, if it doesn't belong here in Issues.

Type synonyms

Can/will type synonyms be added to FFG? And how they should be designed?

I'm willing to implement them if they belong here, but I'm unsure how exactly.
At my fork, I attempted to implement type synonyms as a part of let bindings:

let x = 3
type Test a = List a
let y : Test Natural = [x]
in y

... and while it works perfectly, it doesn't work with module system at all, so there's no way to move type declarations to another file.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.