higherorderco / kind Goto Github PK

The impression created is that Formality is within striking distance of being a practical functional language for the evm. With the massive benefit of simplicity.

What's needed? Another monad instance that exposes the required affects?

I don't know what this means - an example would be really helpful!

Note: while you can use recursive calls as much as you want, it is wise to treat them as normal variables and use move to pass them to branches. This can be a major optimization in some cases

https://github.com/moonad/Formality/blob/master/DOCUMENTATION.md#recursion

extra case branches are ignored by the typechecker, e.g. both the following examples typecheck with fm

Pair.map<A: Type, B: Type, C: Type>(f: B -> C, p: Pair(A, B)): Pair(A, C)
 case p:
 | _;

Pair.map2<A: Type, B: Type, C: Type>(f: B -> C, p: Pair(A, B)): Pair(A, C)
 case p:
 | _;
 | _;

in both cases, the first hole is correctly filled - both of these reduce to (f) (p) p((p.fst) (p.snd) (new) new(p.fst)(f(p.snd)))

there doesn't seem to be a limit on the number of extra branches, nor what can go in them (e.g. holes, different types)

It does not make much sense, to have a different syntax for values and types:

• It introduces new syntactic noise.
• It goes against spirit of dependent types.

E.G. There should be one notation for:

• Function, Constructor, Data arguments
• Lambda, pattern match, type level arrows

Hi Victor, do you need a js visualization for the formality-core? I just have one which can do interaction combinators [1] and it seems it is easy to adapt for your needs. As I am not competent in the intricacies of your project, I leave the link here. (Also I have to pay back for your nice questions on chemlambda.)

All is needed is to input the rewrite rules in obvious places and to feed the script with a network, presently done by adding it to molLib.js [2].

[1] https://mbuliga.github.io/find-the-quine-step-by-step.html

[2] https://github.com/mbuliga/mbuliga.github.io/blob/master/molLib.js

I'm raising this as a documentation issue.

I want to use Haskell or something Haskell-like, to write segments of code that will run in the browser, and work with existing JavaScript code.
This is basically “The JavaScript problem” mentioned in the "The refreshing simplicity of compiling Formality to anything" article.

I like the examples in Graham Hutton's "Programming in Haskell, second edition" book.
I've been able to implement Hutton's "Binary string transmitter" example in chapter 7 of his book, using Ramda, without too much difficulty.
Most functions require just one line of code.
The Haskell code from the book is available here.
See transmit.hs .

I'm now trying to implement the same example using Formality, but am finding it much more difficult.
Is there a tutorial with some pointers on manually converting Haskell to Formality, or on correspondences between the two?
Do you plan to implement additional Haskell-like functions on top of the Formality base, such as those found in the Hutton example(s)?
Could someone implement a few simple applications, perhaps including the above-mentioned "Binary string transmitter" example, or others that are out there in the Haskell universe?

I like what I've seen of Formality so far.
Ken

The following code doesn't stop while type-checking:

import Base#

T Commutes<T>(f : T -> T -> T)
| commutes(f: T-> T -> T, proof : (a:T,b:T) -> f(a, b) == f(b, a))

main: Commutes(Nat; (a:Nat,b:Nat) => add(a,b))
 	?a

1. I was trying to write affine functions where I can copy elements of any type. I ended up making a CopiableType Type:

T CopiableType<T>
| copiableType(
  copy: T -> Pair(T,T),
  firstProj: (x: T) -> x == pair_fst(__ copy(x));
  secondProj: (x: T) -> x == pair_snd(__ copy(x));
  ) 

Using this I can write functions that use x two times. It would be something like this:

foo(X, c: CopiableType(X), x: X): Pair(X,X)
  case c
  | copiableType => c.copy(x)

If I wanted to use it more times, foo could accept multiple CopiableType(X) , or a CopiableType(CopiableType(X)) to copy the copy function lol.
At first It seemed to me that all types are copiable but then realized that erasures can make a Type not copiable. CopiableType(X) itself is not copiable, but without erasures it would be.
My question is if this could be a buildin part of Formality... Only by looking at a Type one can see if it is copiable or not, and if it is, writing a copy function is trivial using pattern matching. This way it won’t be necessary to pass a copy function everywhere you want to use it. The only drawback that I see is that in the current version of Formality the number of times a term can be used is restricted, maybe the number of times a term is used could be part of the Type itself.

2. It is possible to give a term of the type Not(CopiableType(X)) if X is not copiable?

3. What is the purpose of having the erasure in the Subset type? If I I'm writing a proof using some term of the type p: Nat .such_that. IsEven, then at some point I would need to use p.snd, right? If I should use a Sigma instead, then why having Subsets?

Thank you

The current example on the documentation:

mul2(n : Nat) : Nat
  case n
  | zero => zero
  | succ => succ(succ(mul2(n.pred)))

worksForAllN(n : Nat) : mul2(n) == add(n, n)
  equal(__)

says that the output would be:

Type mismatch.
- Found type... Equal(Nat, add(n, n), add(n, n))
- Instead of... Equal(Nat, mul2(n), add(n, n))

but I received:

[ERROR]
Type mismatch.
- Found type... Equal(Nat, add(^-1, ^-1), add(^-1, ^-1))
- Instead of... Equal(Nat, mul2(n), add(n, n))
- When checking equal(Nat; add(^-1, ^-1);)
- With context:
- n : Nat

Why it is necessary to cover cases that does not occur?

T Vector {A : Type} (len : Nat)
| vcons {len  : Nat, head : A, tail : Vector(A, len)} (succ(len))
| vnil                                                (zero)

// Removes the first element
vtail : {~T : Type, ~len : Nat, vector : Vector(T, succ(len))} -> Vector(T, len)
  case/Vector vector
  | vcons => tail
  | vnil  => vnil(~T) <--- THIS ONE
  : Vector(T, pred(len))

Like the title says:

You can construct IsEven(5) with make_even(2.5) since you switched from integer to floats for Number.

Changing from Number to Nat does fix this issue.

Improve error messages

Recursion is still the trickiest bit of fm-lang because they expose the underlying box system of fm-core. It is common for users to try to write something like this:

main : Word
  nat_to_word(0n4)

Which is wrong, because recursive functions are boxed and must be used inside other boxed definitions, and because they need an explicit call_limit:

#main : !Word
  <nat_to_word*4>(0n4)

The error message given by the incorrect program is completely unhelpful:

Type mismatch.
- Found type... Nat
- Instead of... Ind
- When checking succ(succ(succ(succ(zero))))
- On expression nat_to_word(succ(succ(succ(succ(zero)))))

This happens because the first argument of the recursive function nat_to_word is actually its call_limit, which is an Ind (an inductive Nat) instead of the actual first argument (a Nat). This error is further deteriorated by the fact the compiler shows 0n4 as succ(succ(succ(succ(zero)))).

So, we must improve those messages by changing the formatting of nats and inds, detecting those "wrong programs" that many newcomers will probably try to write, and explaining the correct syntax as a hint right on the messages. Something like:

Type mismatch.
- Found type... Nat
- Instead of... Ind
- When checking 0n4
- On expression nat_to_word(0n4)

Hint: the problem is that you used the recursive function `nat_to_word`
inside the non-boxed definition `main`. You also didn't provide a call 
limit. Annotate the type of main as:

    #main : !Word

Also unbox `nat_to_word` and provide a CALL_LIMIT as:

    <nat_to_word*CALL_LIMIT>

Or just omit the CALL_LIMIT to use 2^256 and write it as:

    <nat_to_word*>

Improve expressivity

Right now, the compiler isn't capable of desugaring recursive functions that use the recursive call more than once on the same branch. For example, this doesn't work:

#pow2*N : !{x : Word} -> Word
  if x .= 0:
    1
  else:
    pow2(x - 1) + pow2(x - 1)
halt: 0

The problem is that this desugars to an application of Ind (the inductive Nat, which is a term like {f,x} f(f(f(x)))) and, thus, can only have one recursive call. In this case, it could instead desugar to an inductive tree like {f,x} f(f(x,x), f(x,x)), allowing 2 recursive calls, or {f,x} f(f(x,x,x), f(x,x,x), f(x,x,x)), allowing 3 recursive calls, and so on. This is complex as it requires us to implement syntax-sugars for arbitrary trees, so, instead of just Ind, we'd have Ind1, Ind2, Ind3, etc. This may also be confusing for the user, so care must be taken to do it in a way that stays our of the user's way.

Hi, I started a haskell implementation of the formality language a few months ago but ran out of bandwidth before I was able to complete it. It's here in case anyone want's to pick up the work: https://github.com/o1lo01ol1o/formality-hs

looking forward to an LLVM target for formality-core :)

OS: Nixos unstable
Formality: 0.3.150

Running/typechecking the following code:

test : Word
  get [a ~ b] = temp
  a

temp : [: Word ~ Word]
  [1 ~ 2]

results in the following error:

ReferenceError: subst_name is not defined
    at typecheck (/nix/store/zhqg3jyrxfpp17jmgbgxkpfzqvvg6vpl-node_formality-lang-0.3.150/lib/node_modules/formality-lang/src/fm-core.js:1093:33)
    at typecheck (/nix/store/zhqg3jyrxfpp17jmgbgxkpfzqvvg6vpl-node_formality-lang-0.3.150/lib/node_modules/formality-lang/src/fm-core.js:1126:38)
    at typecheck (/nix/store/zhqg3jyrxfpp17jmgbgxkpfzqvvg6vpl-node_formality-lang-0.3.150/lib/node_modules/formality-lang/src/fm-core.js:1208:24)
    at typecheck (/nix/store/zhqg3jyrxfpp17jmgbgxkpfzqvvg6vpl-node_formality-lang-0.3.150/lib/node_modules/formality-lang/src/fm-lang.js:2518:10)
    at Object.run (/nix/store/zhqg3jyrxfpp17jmgbgxkpfzqvvg6vpl-node_formality-lang-0.3.150/lib/node_modules/formality-lang/src/fm-lang.js:2531:24)
    at /nix/store/zhqg3jyrxfpp17jmgbgxkpfzqvvg6vpl-node_formality-lang-0.3.150/lib/node_modules/formality-lang/src/main.js:190:34

running it normally results in 2 and with -o in {x0} => x0

Question:
How would i get the first value in test to do some computation with it?
If i change

 get [a ~ b] = temp

to

 get [a, b] = temp

i get

[ERROR]
Mismatched erasure.
- When checking get [a,b] = temp; b

This example (from README.md in section "A Nat theorem") produces a type error

Docs.a_plus_0_is_a(a: Nat): Equal(Nat, Nat.add(a, 0), a)
  case a:
  | Equal.to<Nat, Nat.zero>;
  | let ind = Docs.a_plus_0_is_a(a.pred)
    let app = Equal.apply<Nat, Nat, Nat.add(a.pred, Nat.zero), a.pred, Nat.succ, ind>
    app;
  : Equal(Nat, Nat.add(a.self, 0), a.self);

type error:

I think this line:
let app = Equal.apply<Nat, Nat, Nat.add(a.pred, Nat.zero), a.pred, Nat.succ, ind>
should look like this:
let app = Equal.apply<Nat, Nat, Nat.add(a.pred, Nat.zero), a.pred, Nat.succ>(ind)

Formality is fully compiled to a 400-LOC Interaction-Net Runtime.

Both links are dead. I wasn't sure what to link to instead (fm-net.ts?), so I couldn't do a PR 😄

I would like to be able to do something like fm -t && fm -d to typecheck first, then run.

Could we use process.exit(1) when typechecking fails to indicate that to the shell?

Trying to show a Nat by running fmcio hello on

hello: IO(Unit)
  IO.print(Nat.show,  1)

results in

/usr/lib/node_modules/formality-lang/FormalityCore.js:225
        switch (func.ctor) {
                     ^

TypeError: Cannot read property 'ctor' of undefined
    at reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:225:22)
    at reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:224:20)
    at reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:224:20)
    at reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:227:20)
    at Object.reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:227:20)
    at check (/usr/lib/node_modules/formality-lang/FormalityComp.js:201:18)
    at infer (/usr/lib/node_modules/formality-lang/FormalityComp.js:146:26)
    at infer (/usr/lib/node_modules/formality-lang/FormalityComp.js:140:22)
    at check (/usr/lib/node_modules/formality-lang/FormalityComp.js:247:22)
    at check (/usr/lib/node_modules/formality-lang/FormalityComp.js:239:22)

that example provided in Readme.md in the Introduction section uses String.concat, but trying to run the example results in "undefined reference" error.
fm gives this:

it seems there is no definition for String.concat on moonad.org:

you can use mine if you want

String.concat(a:String, b:String) : String
  case a:
  | b;
  | String.cons(a.head, String.concat(a.tail, b));

For this source:

// main.fm
import Base#

bar(T : Type; x : T) : T
  x

main : Number
  bar(~Number, 42)

I get this error with fm -t:

[PARSE-ERROR]
Unexpected symbol.

I noticed the problem on line 8, col 7, file main.fm:

   4| bar(T : Type; x : T) : T
   5|   x
   6|
   7| main : Number
   8|   bar(~Number, 42)
   9|

But it could have happened a little earlier.
I hope this doesn't affect your deadlines!

(The tilde on line 8 is red and underlined)

Recently, I posted how Formality is now able to fuse native terms, i.e., allowing things such as inc^N(x) (applying binary inc N times to x) have complexity O(log2(N)), as well as allowing runtime fusion of map, fold, filter, zip, etc. There is a small cheating going on on those definitions, though:

let inc(n : Uint) => Uint{
  case n -> Uint
  | O(n) => I(n)
  | I(n) => O(inc(n))
  | Z    => Z
}

Notice that I use inc recursively, which isn't legal and won't be allowed in a future. The right way to do recursion in Formality is to use the fold keyword, available on case patterns, which allows us to express Coq's primitive recursion schemes. But, in order to do that, I'm forced to move Uint{} to inside each case:

let inc(n : Uint) =>
  case n -> Uint
  | O(n) => Uint{I(n)}
  | I(n) => Uint{O(fold(n))}
  | Z    => Uint{Z}

This version is legal, but it un-shares the lambda-headers of the returned value on the λ-encoded compilation, which in turn makes this term not fuse. There is a legal way to express fusible functions:

let inc(d : Nat) => 
  let build_inc_layer(rec : (x : Uint) -> Uint, u : Uint) => Uint{
    case u -> Uint
    | O(u) => I(u)
    | I(u) => O(rec(u))
    | Z    => Z
  }
  case d -> () => (x : Uint) -> Uint
  | S(d) => build_inc_layer(fold(d))
  | Z    => build_inc_layer((u : Uint) => u)

In this case, I receive a "maximum depth" as an extra argument, and fold over that depth instead, using that to generate an Uint -> Uint function in the shape I need. But that is uglier, more complex and less flexible.

I'm not sure what to do. Options include:

• Having structural recursion instead of fold. How complex that would be?

• Figuring out other ways to "allow" the first definition.

• Figuring out a (good) way to express a fusible inc using only fold.

I started the tutorial, ran npm i -g formality-lang (got [email protected]), wrote

import Base@0 open

main : Output
  print("Hello, world!")

into hello.fm, and ran fm hello/main. I received the following output:

Downloading files to `fm_modules`. This may take a while...
[PARSE-ERROR]
[PARSE-ERROR]
[PARSE-ERROR]
ReferenceError: TextEncoder is not defined

I noticed the problem on line 12, col 25:
   5|
   6| import Data.List@0 open
   7| import Data.Maybe@0 open
   8| import Data.Maybe.Control@0 open
   9| import Data.Nat@0 open
  10| import Data.Or@0 open
  11| import Data.String@0 open
  12| import Data.Unit@0 open                      --red line
  13| import Data.Vector2D@0 open
  14|
But it could have happened a little earlier.
If this is hard, consider relaxing. You deserve it!

I noticed the problem on line 4, col 0:
   1| import Algebra@0 as Algebra                      --red line
   2| import Control@0 as Control
   3| import Data@0 as Data
   4| import Induction@0 as Induction                      --red line
   5| import Logic@0 as Logic
   6|
But it could have happened a little earlier.
It takes me some time to process things. Have patience with me!

I noticed the problem on line 1, col 18:
   1| import Base@0 open                      --red line
   2|
   3| main : Output
   4|   print("Hello, world!")
But it could have happened a little earlier.
It takes me some time to process things. Have patience with me!

(--red line added by me to indicate red lines)

Is there a library that wasn't packaged right, or something?

I'm on Windows 10.

(By the way, the randomized flavor text at the bottom of each error chunk was funny for a second or two, but almost immediately became annoying. It distracts from the actual data. If you want to keep it, I'd recommend at least restricting it to once per run, and putting it somewhere out of the thick of things, like right after the error is named.)

Hello there. I was following along with DOCUMENTATION.md, and tried putting the following into a file hello.fm:

import Base#

main : Output
  print("Hello, world!")

Then ran:

➜  helloworld fm hello/main
[PARSE-ERROR]
Attempted to re-define 'main', which is already defined as:
- Parse#x39s/main

I noticed the problem on line 4, col 24, file hello.fm:

   1| import Base#
   2|
   3| main : Output
   4|   print("Hello, world!")
   5|

But it could have happened a little earlier.
My parse-robot brain isn't perfect, sorry.

This produces the error message shown above. Is the documentation out of date?

Because of the removal of dist in 59ef91e, installing with the provided nix instructions doesn't work anymore. Installing works, but when executing fm, it cant find ../dist/cli.

The creator of node2nix has a blog post explaining how to run task runners here.
(At the bottom, with grunt instead of gulp)

the command node2nix -d -i package.json --supplement-input supplement.json works correctly.
but nix-build override.nix -A package wields the following error:

npm WARN prepublish-on-install As of npm@5, `prepublish` scripts are deprecated.
npm WARN prepublish-on-install Use `prepare` for build steps and `prepublishOnly` for upload-only.
npm WARN prepublish-on-install See the deprecation note in `npm help scripts` for more information.

> [email protected] prepublish /nix/store/qwd0b8m39nsnfr804bpmc0kvji3jyin5-node_gulp-cli-2.2.0/lib/node_modhttps://github.com/moonad/Formality/commit/59ef91e387de7707085fb1994efbb80cf6c575caules/gulp-cli
> marked-man --name gulp docs/CLI.md > gulp.1

/nix/store/qwd0b8m39nsnfr804bpmc0kvji3jyin5-node_gulp-cli-2.2.0/lib/node_modules/gulp-cli/node_modules/marked-man/bin/marked-man:8
        if (err) throw err;
                 ^

[Error: ENOENT: no such file or directory, open 'docs/CLI.md'] {
  errno: -2,
  code: 'ENOENT',
  syscall: 'open',
  path: 'docs/CLI.md'
}
npm ERR! code ELIFECYCLE
npm ERR! errno 1
npm ERR! [email protected] prepublish: `marked-man --name gulp docs/CLI.md > gulp.1`
npm ERR! Exit status 1
npm ERR!
npm ERR! Failed at the [email protected] prepublish script.
npm ERR! This is probably not a problem with npm. There is likely additional logging output above.

npm ERR! A complete log of this run can be found in:
npm ERR!     /build/.npm/_logs/2019-12-25T13_28_56_419Z-debug.log

builder for '/nix/store/076740c77bhid7b2cw4wazbsz3l6ywg2-node_gulp-cli-2.2.0.drv' failed with exit code 1
cannot build derivation '/nix/store/cgg9njbis9i8kxin6bmcd1c76j01xm7n-node_formality-lang-0.1.228.drv': 1 dependencies couldn't be built
error: build of '/nix/store/cgg9njbis9i8kxin6bmcd1c76j01xm7n-node_formality-lang-0.1.228.drv' failed

I have to investigate why this error occurs.
Maybe we should/could use the gulp that is already packaged for nix.
After Christmas I should have a bit more time to investigate further...

supplement.json

[
  "gulp-cli"
]

override.nix

{ pkgs ? import <nixpkgs> {}
, system ? builtins.currentSystem
}:

let
  nodePackages = import ./default.nix {
    inherit pkgs system;
  };
in
  nodePackages // {
    package = nodePackages.package.override {
      postInstall = "gulp";
    };
  }

Shouldn't the haskell benchmark use ADT like this:

import Prelude hiding (Bool, True, False, not, map, foldr)

-- NATIVE DATATYPES

-- Bitstring
data Bits
  = O Bits
  | I Bits
  | Z
  deriving Show

-- Natural Number
data Nat
  = Succ Nat 
  | Zero
  deriving Show

-- List of Bitstrings
data List 
  = Cons Bits List
  | Nil
  deriving Show

nat :: Integer -> Nat
nat 0 = Zero
nat n = Succ (nat (n-1))

-- FUNCTIONS

inc :: Bits -> Bits
inc  Z       = I Z
inc (O bits) = I bits
inc (I bits) = I (inc bits)

-- Maps a function over a list
map :: (Bits -> Bits) -> List -> List
map _  Nil        = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

foldr :: (a -> a) -> a -> Nat -> a
foldr _ a  Zero    = a
foldr f a (Succ n) = f (foldr f a n)

-- Applies a function 2^n times to a value
apply_pow2n_times :: (a -> a) -> a -> Nat -> a
apply_pow2n_times f a n = foldr f a (pow2 n)

   where
   mul2 n = foldr (Succ . Succ) Zero n  
   pow2 n = foldr mul2 (Succ Zero) n

-- TEST VALUES

-- The natural number 20
n :: Nat
n = nat 20

-- A string of 32 bits, all zeroes
zero :: Bits
zero = foldr O Z (nat 32)

-- A list with 1000 strings of 32 bits, all zeroes
list :: List
list = foldr (Cons Z) Nil (nat 1000)

-- MAIN

-- Maps `inc` 2^20 times to `list`; in total, `inc` is applied 2^20*1000 = 1,048,576,000 = about 1 billion times
main :: IO ()
main
  = print
  $ apply_pow2n_times (map inc) list n

From my experience, the dot notation extremely improves the readability of code, while it is very easy to implement.

The rule:

foo(a,b,c) == a.foo(b,c)

The code:

let four
    Nat.zero . Nat.succ() . Nat.succ() . Nat.succ() . Nat.succ()

-- LABS algorithm
let labs(x : Bits) => Nat
    let xs(k : Nat) => Stream(Bits)
        xs(Nat.succ(k)) . Stream.cons(x . shift(k))

    let autocorrelation(x2 : Bits) => Nat
        Bits.and(x, x2) . popCount()

    xs(0) . map(.autocorrelation().pow(2)) . takeWhile(.equals(0).not()) . sum()

I do not see TypData has any "sort level" compared to Agda or Idris.

I wrote a program so bad that it makes Formality fail to give an error message.

$ head head.fm
head.splitc(c: Char, xs: List(Char)): List(List(Char))
    case xs:
    | nil => List.nil<List(Char)>;
    | cons => if U16.eql(xs.head, c)
        then List.cons<>(c, head.splitc(c, xs.tail))
        else head.splitc(c, xs.tail);

head.splitc_example3 :  _
  head.splitc('x', ['a', 'x', 'b'])



$ fmio head.splitc_example3
(node:4113) UnhandledPromiseRejectionWarning: TypeError: Cannot read property 'comp' of undefined
    at check (/home/bukzor/repo/Formality/node_modules/formality-lang/FormalityComp.js:273:27)
    at check (/home/bukzor/repo/Formality/node_modules/formality-lang/FormalityComp.js:243:24)
    at check (/home/bukzor/repo/Formality/node_modules/formality-lang/FormalityComp.js:243:24)
    at Object.core_to_comp (/home/bukzor/repo/Formality/node_modules/formality-lang/FormalityComp.js:283:23)
    at Object.compile (/home/bukzor/repo/Formality/node_modules/formality-lang/FormalityToJS.js:642:32)
    at Object._io_ (/home/bukzor/repo/Formality/node_modules/formality-lang/bin/lib.js:208:18)
(Use `node --trace-warnings ...` to show where the warning was created)
(node:4113) UnhandledPromiseRejectionWarning: Unhandled promise rejection. This error originated either by throwing inside of an async function without a catch block, or by rejecting a promise which was not handled with .catch(). To terminate the node process on unhandled promise rejection, use the CLI flag `--unhandled-rejections=strict` (see https://nodejs.org/api/cli.html#cli_unhandled_rejections_mode). (rejection id: 1)
(node:4113) [DEP0018] DeprecationWarning: Unhandled promise rejections are deprecated. In the future, promise rejections that are not handled will terminate the Node.js process with a non-zero exit code.

Omnipresent type signatures make example code hard to read.

• Check code on EA-TT. It is different from the one we used on Gitlab.
• FM-Core is about Formality-Core so is very outdated. It is necessary to review its content.
• tutorial.md is a Tutorial about Formality-Core. Will we keep it?

In Formality, the identity type and the rewrite (transp) operation are, like all other datatypes, implemented using self types:

// The Equal datatype.
T Equal <A: Type> (a: A) ~ (b: A)
| to                     ~ (a);

// If a == b, then, P(a) implies P(b)
Equal.rewrite<A: Type, a: A, b: A, P: A -> Type>(e: Equal(A,a,b), x: P(a)): P(b)
  case e:
  | x;
  : P(e.b);

The problem is that, since, inside Equal.rewrite, e is used in a computational position, it appears at runtime. That means equality proofs and casts can't be completely erased from runtime as would be desired. How can this problem be avoided?

T Number { lte : Number -> Number -> Type}      
| cut                  
   { left : Number(lte) 
   , right : Number(lte)   
   , ord : lte(left, right)
  }

produces

RangeError: Maximum call stack size exceeded
    at Typ (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:38:47)
    at unquote (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:776:26)
    at norm (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:887:18)
    at typecheck (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:1382:30)
    at typecheck (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:1426:9)
    at typecheck (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:1666:37)
    at typecheck (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:1405:22)
    at typecheck (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:1405:22)
    at typecheck (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:1426:9)
    at typecheck (/nix/store/lmbq47v660mf4svs6j9qn62p2p897ix7-node_formality-lang-0.3.117/lib/node_modules/formality-lang/src/fm-core.js:1666:37)

Hi, I'm super excited about this project!
I don't know if I'm doing something wrong, but defining the following (from the examples)

data Bool : Type
| true : Bool
| false : Bool

data Nat : Type
| succ : (n : Nat) -> Nat
| zero : Nat

data Eq<A : Type> : (x : A, y : A) -> Type
| refl : (x : A) -> Eq(x, x)

let n0 Nat.zero
let n1 Nat.succ(n0)

the following happens
let stc Eq<Nat>(n0, n0) evaluates to Eq<Nat>(Nat{zero})(Nat{zero}) whereas
let sntc Eq<Nat>(n0, n1) evaluates to Eq<Nat>(Nat{zero})(Nat{succ(Nat{zero})}). I thought that this should return a type error?

Or should I construct Equalities in a different way? refl doesn't seem to help, as it only takes one argument

Thanks so much!

Formality Version: 03.123

When running the following code (a naive implementation for project euler problem 1), i get different results when executing the main function normally and with -o/-O:

import Base@0

#create_step_list*N : ! {step : Word, limit : Word, acc : Word} -> List(Word)
  if acc .< limit:
    cons(~Word, acc, create_step_list(step, limit, acc + step))
  else:
    nil(~Word)
halt: nil(~Word)

main : Word
  let list3  = <create_step_list*>(3, 1000, 3)
  let list5  = <create_step_list*>(5, 1000, 5)
  let list15 = <create_step_list*>(15, 1000, 15)
  let concatenated_list = <concat*>(~Word, list3, list5)
  let concatenated_sum = <sum*>(concatenated_list)
  let duplicate_sum = <sum*>(list15)
  concatenated_sum - duplicate_sum

> fm main/main -t
Word
> fm main/main   
233168
> fm main/main -O
4294967284

The program below:

id<A:Type>(x:A): A
  x

T Bool
| true;
| false;

T The(A: Type) ~ (x: A)
| new(x: A) ~ (x);

foo: Bool
  id<Bool>(?a)

bar: The(Bool, Bool.true)
  The.new<Bool>(foo)

Type-checks, but the generated .fmc files don't. The reason is that ?a is filled as Bool.false when foo is type-checked. Then, when type-checking bar, that information is lost and it is filled as Bool.true. The generated foo.fmc gets ?a = Bool.false, causing bar not to type-check.

This can be solved by reusing past hole fillings when type-checking separate definitions.

This has a recursive call inside each case

toBrainFuck(p : List(Instruction)) : String
case p
| nil => nil()
| cons =>
case p.head as ins
| right => cons( '>', toBrainFuck(p.tail))
| left => cons(_ '<', toBrainFuck(p.tail))
| inc => cons(_ '+', toBrainFuck(p.tail))
| dec => cons(_ '-', toBrainFuck(p.tail))
| write => cons(_ '.', toBrainFuck(p.tail))
| read => cons(_ ',', toBrainFuck(p.tail))
| loop => concat(_ concat(_ cons(_ '[' , toBrainFuck(ins.code)), "]"), toBrainFuck(p.tail))

So, when compiled to JS, every case would recurse, being accidentally exponential.

A temporary solution: insert + toBrainFuck : List(Instruction) -> String inside toBrainFuck, below the second case.
This will pass the recursive calls linearly to each branches, preventing this problem from happening. it is also a very good practice in general, interaction nets like that style.

On the long term, we can make the JS compiler lazy by wrapping every value inside a ()=>... closure

How do I make this program work?

import Base#

laver(a:Nat, b:Nat) : Nat
if a==0 then b else if b==3 then a-1 else laver(laver(a,b+1),a-1)

main : Nat
laver(3,1)

When run with fm -d main/main I always get
(node:67386) UnhandledPromiseRejectionWarning: RangeError: Maximum call stack size exceeded

Changing Nat to Number gives (node:67400) UnhandledPromiseRejectionWarning: TypeError: Cannot read property '0' of undefined

From https://github.com/moonad/Formality , clicking on https://docs.formality-lang.org in the description leads to a notification that "We moved to Github!", and clicking on the provided link https://github.com/moonad/Formality/blob/master/DOCUMENTATION.md yields a 404. So...where's the documentation?

This snippet from my current work-in-progress on first-class modules:

T Elem <A : Type>                                      ~ (x: A, xs : List(A))
| Elem.here<x: A, xs: List(A)>                         ~ (x, List.cons<A>(x,xs));
| Elem.there<x: A, y: A, xs: List(A),e: Elem(A,x,xs)> ~ (x, List.cons<A>(y,xs));

str : List(String)
  ["foo","bar"]

testElem : Elem(String, "foo", str)
  Elem.here<String,"foo", ["bar"]>

This compiles, but inlining str causes

Found 1 type error(s):

Inside testElem:
Unfilled hole: TW.

Λ ➜ fm -v              
0.1.208

The following file

import Base#

main(n : Nat) : Nat
  log(true)
  ?a

when type-checked:

Λ ➜ fm -t Log
Found hole: 'a'.
- With goal... Nat
- Couldn't find a solution.
- With context:
- n : Nat

(n : Nat) -> Nat ✔

This replicates with returning a hole or a value. Curiously, a hole in the log is detected:

import Base#

main(n : Nat) : Nat
  log(?b)
  ?a

Found hole: 'b'.
- Couldn't find a solution.
- With context:
- n : Nat

I think maybe the documentation (and possibly the implementation) changed regarding recursive functions - I had some test functions defined so:

!mul2*N : !{case n : Nat} -> Nat
| succ => succ(succ(mul2(n)))
| zero => zero
* zero

This worked a week or two ago, but I believe that the initial ! should now be a #. This is fine. However, the compiler does not tell me that's the problem. What it tells me is that that function and all functions after are undefined:

> fm hello/natmain
Definition not found: hello/natmain

The compiler should probably, instead, tell me that the definition of mul2 is incorrect.

The documentation states

if n: a else: b | If n .= 0, evaluates to a, else, evaluates to b

According to the segment above that, .= means "equals". So, if n equals 0, n should effectively mean "true". However, in testing:

print(if 0: "0:true" else: "0:false") prints 0:false
print(if 1: "1:true" else: "1:false") prints 1:true

which seems opposite what the documentation says.

Because types are corecursively defined, to check whether those types are equal, we cannot just normalize them and check whether their normal forms are definitionally equal. Rather, we attempt to reduce redexes in all possible orders, branching and performing a breadth-first search. However, the problem with this is that type checking some code like

nat.test0: The(Nat, 100n)
  the(_ add(50n, 50n))

is incredibly (exponentially) slow, since it will try to reduce add(50n, 50n) in all possible orders. A better solution would be to normalize the term before.

How should we prevent the type checker from doing the slow search when it isn't needed? As a possible direction to the solution of this problem I stress that while types are corecursively defined, terms are recursively defined, so that we might need different strategies depending on whether we are dealing with a term or a type.

The following typechecks and runs fine:

T Thing
| thing

main: Thing
  case thing
  | thing => thing

But this does not:

main: Thing
  case thing
  | thing => thing

T Thing
| thing

It gives the following parse error (the space between "case" and "thing" on line 2 is highlighted):

tmp$ fm -t
[PARSE-ERROR]
Couldn't find the ADT for this pattern-match.
Make sure the cases have the correct name and order.

I noticed the problem on line 2, col 7, file main.fm:

   1| main: Thing
   2|   case thing
   3|   | thing => thing
   4|
   5| T Thing
   6| | thing

Since they're both backwards they cancel out if you're only doing string stuff with literals - but if you attempt to construct character programmatically it becomes clear.
Specifically, the Bits type is little endian - the least significant bit is what can be deconstructed with a top-level case statement. But the parser and the show function both treat it as big endian.

main : Bits
  'a'

Bits ✔
(be, b0, b1) => b1((be, b0, b1) => b1((be, b0, b1) => b0((be, b0, b1) => b0((be, b0, b1) => b0((be, b0, b1) => b0((be, b0, b1) => b1((be, b0, b1) => be)))))))

So, this looks like 0b1100001, or 97 - ascii 'a'.
But, if you increment it:

main : Bits
  inc_bits('a')

Bits ⚠
(be, b0, b1) => b0((be, b0, b1) => b0((be, b0, b1) => b1((be, b0, b1) => b0((be, b0, b1) => b0((be, b0, b1) => b0((be, b0, b1) => b1((be, b0, b1) => be)))))))

Incrementing to 0b0010001 doesn't make sense! But, it is actually incrementing a little-endian integer from 0b1000011 to 0b1000100.

I found this while trying to write a print_nat function.

I think I can PR a fix for this in the next few days if no one else does it first

I think the title is self explanatory, I read the code and there are various places where a variable wont change and still it is declared with var.

Also, places where a variable could change, IMO should use let over var, to get scope benefits.

> fm --version
 0.1.200

I get an error (sometimes) when i want to typecheck the code in the gist.
Not all the time, but somewhere around the size of the current string it happens somewhat consistently.
Sometimes it typechecks correctly.

> fm main/values -t
RangeError: Maximum call stack size exceeded
    at quote (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:468:52)
    at reduce (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:484:16)
    at weak_normal (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:769:12)
    at typecheck (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:832:23)
    at typecheck (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:951:22)
    at typecheck (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:951:22)
    at typecheck (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:951:22)
    at typecheck (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:951:22)
    at typecheck (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:951:22)
    at typecheck (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-core.js:951:22)
Sorry, the type-checker couldn't handle your input.

When i execute it with interaction nets it take a few seconds, then outputs a similar error.

fm main/values -o
RangeError: Maximum call stack size exceeded
    at Array.push (<anonymous>)
    at build_term (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-to-net.js:214:24)
    at build_term (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-to-net.js:225:26)
    at build_term (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-to-net.js:215:26)
    at build_term (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-to-net.js:215:26)
    at build_term (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-to-net.js:225:26)
    at build_term (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-to-net.js:215:26)
    at build_term (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-to-net.js:215:26)
    at build_term (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-to-net.js:225:26)
    at build_term (/nix/store/5g7mgyjih6gcmvqj1jni7g5lgxa9v1iy-node_formality-lang-0.1.200/lib/node_modules/formality-lang/src/fm-to-net.js:215:26)
{"rewrites":19466,"loops":21149303,"max_len":21091}

Does the same happen with the new implementation of the interaction nets?

F64.Ordering : Type
  F64.ordering<P: F64.Ordering -> Type> ->
  (LT: P(F64.Ordering.LT)) ->
  (EQ: P(F64.Ordering.EQ)) ->
  P(F64.ordering)

T F64.Ordering
| LT;
| EQ;
| GT;

Having the code above in the same file does not accuse a redeclaration of type.

Given the file:

HelloWorld.fm

import Base#

main : Number
  1

Then we compile with:

fm -J HelloWorld/main

The output code is:

(function(){
  return undefined;
})()

I already figured out how to fix it. I'll make a PR right now.