Types are an extremely powerful notion in programming as what is behind types is logic itself. However, making effective use of types in programming is a very difficult task for many programmers (ranging from novices to experts). In this article, I will present several solutions to a simple problem, gradually illustrating certain typical uses of dependent types and linear types in programming.
Given three poles: Pole 1, Pole 2 and Pole 3, there are 64 disks of distinct sizes stacked on Pole 1 such that no disk is stacked on one of a lesser size, and both Pole 2 and Pole 3 are empty. The player is asked to finish the task of moving all the disks from Pole 1 to Pole 2 (while using Pole 3 as a spare): Only one disk can be moved from one pole to another one at any time and no disk is ever allowed to be stacked on another one of a lesser size during the entire process of disk-moving.
It will soon be clear that 264-1 moves are needed in order to accomplish the aforementioned task. Please click here to see a simple demo where there are 8 disks initially stacked on Pole 1.
First, let us see a straightforward solution of imperative style to the Hanoi Towers puzzle. A datatype pole is declared as follows for representing poles:
datatype pole = Pole of ( string(*name*), ref(list0(int))(*disks*) ) (* end of [Pole] *)Note that the disks stacked on a pole is represented as a list of integers. As a disk may be moved from one pole to another one, a reference to a list of integers is contained in the representation of a pole so that the content of the reference can be updated to reflect the actual disks stacked on the pole.
In the following code, the function move_1 is called to move a single disk from one pole to another one:
// extern fun move_1(P1: pole, P2: pole): void // implement move_1(P1, P2) = let // val Pole(n1, r1) = P1 val-cons0(x, xs) = !r1 val ((*void*)) = !r1 := xs // val Pole(n2, r2) = P2 val ((*void*)) = !r2 := cons0(x, !r2) // in println! ("Move [", x, "] from [", n1, "] to [", n2, "]") end // end of [move_1] //The function move_n for moving multiple disks from one pole to another one (while using the third one as a spare) can be implemented based on move_1 as follows:
// extern fun move_n ( n: int , P1: pole, P2: pole, P3: pole ) : void // implement move_n ( n, P1, P2, P3 ) = ( // if n > 0 then { val n1 = n - 1 val () = move_n(n1, P1, P3, P2) val () = move_1(P1, P2) val () = move_n(n1, P3, P2, P1) } // ) (* end of [move_n] *) //
It is easy to see that move_n, when applied a natural number N and 3 distinct poles, makes 2N-1 calls to move_1 before it returns.
A serious issue with the above solution (of imperative style) is that pattern matching involved in the following val-declaration (appearing inside the body of move_1) is not guaranteed (solely based on typechecking) to succeed:
val-cons0(x, xs) = !r1
While the use of a reference in the type pole makes it
straightforward to implement move_1, reasoning about the
implementation of move_1 is greatly complicated (largely
due to the involvement of a global state).
Let us see as follows a solution of functional style to the Hanoi Towers puzzle that rules out (solely based on typechecking) the possiblity of pattern matching failure at run-time.
Given an integer N, the type pole(N) is for a pole on which N disks are stacked:
// abstype pole(n:int) = ptr //
The functions move_1 and move_n are given the following types to reflect their functional nature:
// extern fun move_1 {p1,p2:nat|p1 > 0} ( P1: pole(p1), P2: pole(p2) ) : (pole(p1-1), pole(p2+1)) // extern fun move_n{n:nat} {p1,p2,p3:nat|p1 >= n} ( n: int(n) , P1: pole(p1), P2: pole(p2), P3: pole(p3) ) : (pole(p1-n), pole(p2+n), pole(p3)) //Note that the type assigned to move_1 indicates that move_1 is of functional style: Given two poles holding P1 and P2 disks such that P1 is positive, move_1 returns two (new) poles holding P1-1 and P2+1 disks. Similarly, move_n is also of functional style.
The functions move_1 and move_n of functional style are implemented as follows:
local datatype pole_(n:int) = Pole of ( string, list(int, n) ) (* end of [pole_] *) assume pole(n:int) = pole_(n) in (* in-of-local *) implement move_1(P1, P2) = let // val Pole(n1, r1) = P1 val+list_cons(x, xs) = r1 // no failure! val Pole(n2, r2) = P2 // val () = println! ( "Move [", x, "] from [", n1, "] to [", n2, "]" ) (* end of [val] *) // in (Pole(n1, xs), Pole(n2, list_cons(x, r2))) end // end of [move_1] end // end of [local] (* ****** ****** *) implement move_n(n, P1, P2, P3) = ( // if n > 0 then ( P1, P2, P3 ) where { val n1 = n - 1 val (P1, P3, P2) = move_n(n1, P1, P3, P2) val (P1, P2) = move_1(P1, P2) val (P3, P2, P1) = move_n(n1, P3, P2, P1) } else (P1, P2, P3) // ) (* end of [move_n] *)Note that the keyword val+ indicates the need to verify (based on typechecking) the exhaustiveness of pattern matching involved in the val-declaration it introduces.
With no involvement of a global state, reasoning about the functional version of move_1 and move_n is greatly simplified. And this is often claimed as a strong selling point for functional programming.
While functional programming can greatly simplify reasoning, it is often wasteful in terms of memory usage. For instance, each call to the above functional version of move_1 builds two new poles; the two poles passed as arguments are of no more use after the call returns. Fortunately, one can turn to what I refer to as linear functional programming in ATS to reduce or even eliminate this kind of waste.
Let us first declare pole as a linear type:
// absvtype pole(n:int) = ptr //Unlike a non-linear type, a value of a linear type can be modified. The types for the linear functional version of move_1 and move_n are declared as follows:
// extern fun move_1 {p1,p2:nat|p1 > 0} ( P1: !pole(p1) >> pole(p1-1) , P2: !pole(p2) >> pole(p2+1) ) : void // end-of-function // extern fun move_n{n:nat} {p1,p2,p3:nat|p1 >= n} ( n: int(n) , P1: !pole(p1) >> pole(p1-n), P2: !pole(p2) >> pole(p2+n), P3: !pole(p3) ) : void // end-of-function //Based on the type of move_1, it is clear that calling the function on two given poles P1 and P2 changes the types of these two poles to reflect the fact that P1 contains one fewer disk after the call and P2 one more disk. The type assigned to move_n can be interpreted similarly.
The functions move_1 and move_n of linear functional style are implemented as follows:
local // datavtype pole_(n:int) = Pole(n) of ( string, list_vt(int, n) ) (* end of [pole_] *) // assume pole(n:int) = pole_(n) // in (* in-of-local *) implement move_1(P1, P2) = let // val+@Pole(n1, rxs) = P1 val n1 = n1 val+~list_vt_cons(x, xs) = rxs val ((*void*)) = rxs := xs prval ((*folded*)) = fold@(P1) // val+@Pole(n2, rxs) = P2 val n2 = n2 val ((*void*)) = rxs := list_vt_cons(x, rxs) prval ((*folded*)) = fold@(P2) // in println! ("Move [", x, "] from [", n1, "] to [", n2, "]") end // end of [move_1] end // end of [local] (* ****** ****** *) implement move_n(n, P1, P2, P3) = ( // if n > 0 then () where { // val n1 = n - 1 val () = move_n(n1, P1, P3, P2) val () = move_1(P1, P2) val () = move_n(n1, P3, P2, P1) // } (* end of [then] *) else () // end of [else] // ) (* end of [move_n] *)Note that a pole now contains a linear list. In contrast to the (non-linear) functional version of move_1, the linear functional version of move_1 returns two new poles that are built by modifying the two poles passed as arguments: There is no waste in this case as the original poles are no longer in existence after the call to move_1 is returned.
For the entirety of the three presented solutions to the Hanoi Towers puzzle, please visit the following files:
This article is written by Hongwei Xi.