DEV Community: Masaki Haga

How to Prepare Rational Numbers to Handle Fractions in Standard ML

Masaki Haga — Thu, 26 Mar 2020 00:52:00 +0000

Let's implement a data type like Data.Ratio of Haskell in Standard ML that will handle rational numbers (with greater precision than floating point).

signature

signature RATIO =
sig
    type ratio = int * int
    exception DivideByZero
    val fromIntPair : int * int -> ratio
    val + : ratio * ratio -> ratio
    val - : ratio * ratio -> ratio
    val * : ratio * ratio -> ratio
    val / : ratio * ratio -> ratio
    val > : ratio * ratio -> bool
    val < : ratio * ratio -> bool
end

The name of data type is ratio. It is actually a couple of integer.
Prepare conversion functions fromIntPair, addition, subtraction, multiplication and division of fractions, and comparison operations.
In practice this is a couple of integer, so use = for the equal sign.

structure

structure Ratio : RATIO =
struct
type ratio = int * int
exception DivideByZero
fun fromIntPair (num, 0) = raise DivideByZero
  | fromIntPair (0, den) = (0, 1)
  | fromIntPair (num, den) =
    let fun gcd (x, y) = if x = y then x
                 else if x > y then gcd (x - y, y)
                 else gcd (x, y - x)
        val g = if den > 0 then gcd (abs num, abs den)
                else ~(gcd (abs num, abs den))
    in (num div g, den div g)
    end
fun (x, y) + (z, w) = fromIntPair (Int.+(Int.*(w, x), Int.*(y, z)), Int.*(y, w))
fun (x, y) - (z, w) = fromIntPair (Int.-(Int.*(w, x), Int.*(y, z)), Int.*(y, w))
fun (x, y) * (z, w) = fromIntPair (Int.*(x, z), Int.*(y, w))
fun (x, y) / (z, w) = fromIntPair (Int.*(x, w), Int.*(y, z))
fun (x, y) > (z, w) = Int.>(Int.*(w, x), Int.*(y, z))
fun (x, y) < (z, w) = Int.<(Int.*(w, x), Int.*(y, z))
end

The argument to fromIntPair will call an exception if the denominator is 0, and return (0, 1) if the numerator is 0.
Otherwise, the greatest common divisor is obtained by taking the absolute value and dividing by the greatest common divisor obtained by the numerator and the denominator.
If the denominator is negative, the sign is reversed because only the numerator is signed.

In the four arithmetic operations of fractions, the numerator is calculated with the denominator aligned and then reduced with fromIntPair.
In comparison operations, the numerators are compared after the denominators are aligned.

example

Use open to expand a structure, and use local to avoid hiding the constraints of the original four operations and comparisons.

- local open Ratio
= in
= val twoThird =
= let val oneThird = fromIntPair (1, 3)
= in oneThird + oneThird
= end
= end
= ;
val twoThird = (2,3) : int * int

How to Creat Executable Commands in Standard ML

Masaki Haga — Wed, 25 Mar 2020 18:59:52 +0000

Standard ML programs are often used in interactive shells(?) However, we can not only use it in an interactive shell, but also compile it to create executable commands.

To get a command name and arguments

In Standard ML, CommandLine structure provides name function and arguments. Command names and command line arguments will be obtained by them.

`name` function

— CommandLine.name;
val it = fn: unit -> string

CommandLine.name () yields the command name as a string.

`arguments` function

- CommandLine.arguments;
val it = fn: unit -> string list

CommandLine.arguments () gives command line arguments as a list of string types.

Termination process

To close the program and return to the shell, use the Process.exit function of OS structure.

- OS.Process.exit
val it = OS.Process.status -> 'a

The argument OS.Process.status is an exit status data type to pass to the shell. There are two types:

OS.Process.success: Success (Corresponds to EXIT_SUCCESS in C)
OS.Process.failure: Failure (Corresponds to EXIT_FAILURE in C)

To run a program

val arg = someFunc1
val _ = (someFunc2 arg; ...)

You can execute defined functions by evaluating them at the top level. The return value of functions should be discarded using an underscore or serial execution if they only use side effects.

Example

If you compile it with mlton, it becomes an executable.

(* someCommand.sml *)
val n = ref 0
fun prName () = print ("Name: \n" ^ CommandLine.name () ^ " \n")
fun prArg () = foldl (fn (z, unt) => print ((n := !n + 1; Int.toString (!n)) ^ ":" ^ z ^ " \n")) (print "Arguments: \n") (CommandLine.arguments ())
val _ = (prName (); prArg (); OS.Process.exit (OS.Process.success))

$ mlton someCommand.sml
$ ./someCommand a b c d
Name:
./someCommand
Arguments:
1: a
2: b
3: c
4: d

Reference

sml-family.org (Standard ML Main Site)

Even though you've been using Emacs for a long time, you usually use arrow keys, you shouldn't edit the file.

Masaki Haga — Wed, 25 Mar 2020 18:42:05 +0000

Stupid people who always use arrow keys to control cursors are not entitled to edit the file. (I was inspired by this article.)

(global-set-key [up] 'kill-emacs)
(global-set-key [down] 'kill-emacs)
(global-set-key [left] 'kill-emacs)
(global-set-key [right] 'kill-emacs)

Behavior	Key Binding	How to remember
Move Cursor 1 Line Up	C-p	preverious
Move Cursor 1 Line Down	C-n	next
Move Cursor 1 Character to Left	C-b	backward
Move Cursor 1 Character to Right	C-f	forward

Note: This is a joke. Unlike save-buffers-kill-terminal, which is assigned to C-x C-c, kill-emacs forces Emacs to drop without warning even if it has not been saved. I will not be responsible for the loss of important edited data if automatic backup is turned off.

Installing Agda using Stack

Masaki Haga — Wed, 25 Mar 2020 18:04:56 +0000

I recently installed Agda on my Linux machine, so I'll take note of what I did.

Install `alex`, `happy`

alex is a tool to generate a lexical analyzer and happy is a parser generator. (They correspond to lex and yacc respectively.)

$ stack install alex happy

Install `Agda`

$ stack install Agda

I failed to compile with an error message.

Add to `stack.yaml` and install `Agda` again

Refer to the following part of the error message and add the following to ~/.stack/global-project/stack.yaml:

Some different approaches to resolving this:

* Recommended action: try adding the following to your extra-deps in/home/(Username)/.stack/global-project/stack.yaml:

- hogehoge
- hugahuga
(Omitted)

Plan construction failed.

However, if you already have extra-deps:, add:

extra-deps:
- hogehoge
- hugahuga
(Omitted)

Install Agda again, repeat if it fails, and proceed if it succeeds.

Set `agda-mode` to work with `Emacs`

$ agda-mode setup && agda-mode compile

Install`Standard Library`

Version 1.1 has been installed.

$ mkdir -p ~/.agda/lib
$ cd ~/.agda/lib
$ wget https://github.com/agda/agda-stdlib/archive/v1.1.tar.gz
$ tar xvzf v 1.1 .tar.gz
$ echo "$HOME/.agda/lib/agda-stdlib -1.1/standard-library.agda-lib" > ~/.agda/libraries

$ agda-I-l standard-library

It's over. Yay! (^○^)