More examples please

[kenwebb]

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

[johnchandlerburnham]

Hi! Thanks so much for your question!

We're currently working hard to finalize the Formality language specification by implementing Formality in itself. This is going to change a lot of things, so we're holding off on writing documentation and examples until that's done. I really like the Graham Hutton book a lot and am planning on writing a tutorial for Formality in that style.

However, since I don't want to leave you hanging, I'll walk you through how you could do transmit.hs in the current Formality. Just be advised that lots of this stuff is going to change.

So my first pass was to try to just directly translate the conversions functions:

import Base#

Bit : Type; Number

bin2int(xs: List(Bit)) : Number
  fold(__ 0, (x,y) => x + (2 * y) xs)

int2bin(x: Number) : List(Bit)
  let x = x >>> 0
  if x === 0 then nil(_)
  else cons(_ (x % 2), int2bin(x \ 2))

But there are a couple weird things about this. First, since Number is just JavaScript's number, we have to do the weird >>> 0 thing to get the division function (yes, that's a \ not a /, it's from a bad/temporary parsing hack and we're changing it) to do the right thing.

We think Number is going to go away as a Formality-Core primitive in Formality 1.0, but we'll have Word for integers and Double for floating point on the front-end language. Haven't totally decided yet, stay tuned.

Anyway, my second approach on transmit.fm was to use Formality's Bits bitstream type for some type-safety:

T Bits
| be
| b0(pred : Bits)
| b1(pred : Bits)

This let me write encode by turning Chars (which are just Numbers) into continuations:

encodeChar(x : Char) : Bits -> Bits
  let x = x >>> 0
  if x === 0 then b0
  else
    if (x % 2) === 0
    then (y) => b0(encodeChar(x \ 2)(y))
    else (y) => b1(encodeChar(x \ 2)(y))

encode(x : String) : Bits
  case x
  | nil  => be
  | cons => encodeChar(x.head)(encode(x.tail))

Then for decode we need some library functions that weren't implemented yet:

bits_to_number(x : Bits) : Number
  case x
  | be => 0
  | b0 => 0 + (bits_to_number(x.pred) << 1)
  | b1 => 1 + (bits_to_number(x.pred) << 1)

bits_to_number(x : Bits) : Number
  case x
  | be => 0
  | b0 => 0 + (bits_to_number(x.pred) << 1)
  | b1 => 1 + (bits_to_number(x.pred) << 1)

bits.take(n : Number, x : Bits) : Bits
  let n = n >>> 0
  if n === 0 then be
  else
    case x
    | be => be
    | b0 => b0(bits.take(n - 1, x.pred))
    | b1 => b1(bits.take(n - 1, x.pred))

bits.drop(n : Number, x : Bits) : Bits
  let n = n >>> 0
  if n === 0 then x
  else
    case x
    | be => be
    | b0 => bits.drop(n - 1, x.pred)
    | b1 => bits.drop(n - 1, x.pred)

chop8(x : Bits) : List(Bits)
  case x
  | be => nil(_)
  | b0 => cons(_ bits.take(8, x), chop8(bits.drop(8,x)))
  | b1 => cons(_ bits.take(8, x), chop8(bits.drop(8,x)))

decode(x : Bits) : String
  map(__ bits_to_number, chop8(x))

And finally a main for testing:

main : String
  decode(encode("foobar"))

To test, we can do:

$ fm -d transmit
"foobar"

Now for an exercise:

I have deliberately left a bug in the above example which you can see with

main : String
  decode(encode("ba;dddd"))

$ fm -d transmit
"ba;2222"

Eternal fame and glory if you can figure out why this happens and want to post the fix here.

In any event, I'll push the correct version to Base.fm when I add the String -> Bits library functions in the next day or two.

[kenwebb]

Excellent! I'll watch for the updates to Base.fm.

[johnchandlerburnham]

Looks like @MaiaVictor beat me to it on https://github.com/moonad/Base.fm/blob/42fac6a19ae87dd46adf9176531118ceb2967948/String.fm

My solution to the transmit.fm bug is here: https://gist.github.com/johnchandlerburnham/efeccd2c038ce975813e34c9ca46777d

[kenwebb]

I played around with @johnchandlerburnham gist. I had to change the imports. It worked for me with Formality-Lang v0.1.252 My updated gist is here Thank you.

[johnchandlerburnham]

Yeah, looks like you used my solution gist. The original bug was with

encodeChar(x : Char) : Bits -> Bits
  let x = x >>> 0
  if x === 0 then b0
  else
    if (x % 2) === 0
    then (y) => b0(encodeChar(x \ 2)(y))
    else (y) => b1(encodeChar(x \ 2)(y))

This needed the bits to be padded in groups of 8 so the correct version is

encodeChar(len : Number, x : Number) : Bits -> Bits
  let x = x >>> 0
  if x === 0 then 
    if len > 1 then (y) => b0(encodeChar(len - 1, x)(y))
    else b0
  else
    if (x % 2) === 0
    then (y) => b0(encodeChar(len - 1, x \ 2)(y))
    else (y) => b1(encodeChar(len - 1, x \ 2)(y))

Looks like you found a few more bugs though. I think the continuation approach is probably just finicky. Better to do

string_to_bits(str: String) : Bits
  case str
  | nil =>
    be
  | cons =>
    let char_bits = number_to_bits(16, str.head)
    let rest_bits = string_to_bits(str.tail)
    concat_bits(char_bits, rest_bits)

which is now in Base.fm: https://github.com/moonad/Base.fm/blob/42fac6a19ae87dd46adf9176531118ceb2967948/String.fm#L42

[VictorTaelin]

Formality was refactored, we're making a new documentation!