bukzor

$ pyright mycode_test.py
pyright 1.1.261
./mycode_test.py
  ./mycode_test.py:42:16 - error: Cannot assign member "slow_method" for type "Gizmo"
    Expression of type "() -> Literal[3]" cannot be assigned to member "slow_method" of class "Gizmo"
      Type "() -> Literal[3]" cannot be assigned to type "() -> Frob"
        Function return type "Literal[3]" is incompatible with type "Frob"
          "Literal[3]" is incompatible with "Frob" (reportGeneralTypeIssues)
1 error, 0 warnings, 0 informations 

bukzor

>>> i = 0x12000
>>> while True:
...   i, c, name = i + 1, chr(i), unicodedata.name(chr(i))
...   print(i, c, name)
...
73729 𒀀 CUNEIFORM SIGN A
73730 𒀁 CUNEIFORM SIGN A TIMES A
73731 𒀂 CUNEIFORM SIGN A TIMES BAD
73732 𒀃 CUNEIFORM SIGN A TIMES GAN2 TENU
73733 𒀄 CUNEIFORM SIGN A TIMES HA

bukzor

$ cd "$(mktemp -d)"

$ ln -sf realpath symlink

$ mkdir realpath

$ cd symlink

$ touch foo.py

bukzor

This kinda-sorta works:

$ cd share/Formality/

$ git diff
diff --git a/javascript/FormalityToJS.js b/javascript/FormalityToJS.js
index c2dc6a1..2089d39 100644
--- a/javascript/FormalityToJS.js
+++ b/javascript/FormalityToJS.js

bukzor

cat.IO.readline<A: Type>(_: A): IO(String)
  use line = IO.ask<String>("get_line", "")
  IO.end<String>(line)

cat.go<A: Type>(io: IO(A)): IO(Unit)
  get bind pure = IO.monad
  let io1 = bind<,>(io, cat.IO.readline<>)
  let io2 = bind<,>(io1, IO.print)

  cat.go<>(io2)

bukzor

Type definition

T Color.
| Red.;
| Blue.;

Desugars to:

bukzor

T False

T True
| true;

Not(A: Type): Type
  A -> False

T Equal<A: Type> ~ (a: A, b: A)
| same<a: A> ~ (a, a);

bukzor

$ cat head2.fm

head2.IO.readline(_: Unit): IO(String)
  use line = IO.ask<String>("get_line", "")
  IO.end<String>(line)

head2: IO(Unit)
  get bind pure = IO.monad
  let io0 = pure<>(Unit.new)
  let io1 = bind<,>(io0, head2.IO.readline)

bukzor

$ cat example.fm
example.3.0 : _
  pythonic.str.split("", "abc")

example.3.1 : _
  ["a", "b", "c"]


example.3.test: The(_, example.3.1)
  The.value<>(example.3.0)

bukzor

$ 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'])