[ planet-factor ]

Semantic Versioning (or "semver" for short) is a specification for handling version numbers, and providing a way to sort and specify compatibility using a MAJOR.MINOR.PATCH structure with optional "pre-release" and "build" information.

Some examples of semantic version numbers:

• 1.0.0-alpha
• 1.0.0-beta+win32
• 1.0.0-rc.1
• 1.0.0

For a long time, I thought it might be funny to follow the upcoming release of Factor version 0.99 with version 0.100. Well, if we wanted to be consistent with "semver", it might instead have to be something like 0.100.0-joke+haha.

There is now a semver vocabulary that provides some words for sorting and working with semantic version numbers. Here's an example using it:

IN: scratchpad USE: semver

IN: scratchpad "0.99.0" >semver bump-alpha semver.
0.99.1-alpha.0

IN: scratchpad "0.99.0" >semver bump-preminor bump-rc semver.
0.100.0-rc.0

IN: scratchpad "0.99.0" "0.100.0" semver<=> .
+lt+

IN: scratchpad "0.100.0-joke+haha" >semver bump-major semver.
1.0.0

Reading the Semantic Versioning 2.0.0 specification, it suggests using the version numbers to represent compatibility with previous versions. And many languages have package managers that use these compatibility guarantees with "semver ranges" to manage project dependencies.

Many years ago, there was a blog post containing five programming problems every software engineer should be able to solve in less than 1 hour. I had bookmarked it at the time and didn't notice the controversy it created on Reddit. The original link seems to be down — you can view a copy of it on the Wayback Machine — but there are various solutions posted online, including a solution in Python.

I finally got around to looking at it and writing up some solutions to the problems listed. Apparently, instead of solving this in 1 hour in Factor, it took me almost 8 years:

IN: scratchpad 2015 05 09 <date> days-since >integer .
2814

Problem 1

Write three functions that compute the sum of the numbers in a given list using a for-loop, a while-loop, and recursion.

In idiomatic Factor, this is just sum, and we would typically use sequence combinators, but instead here are a few solutions using lexical variables.

Using a for-loop, iterating forwards:

:: solve-1 ( seq -- n )
    0 seq length [ seq nth-unsafe + ] each-integer ;

Using a while-loop, iterating forwards:

:: solve-1 ( seq -- n )
    0 0 seq length :> n
    [ dup n < ] [
        [ seq nth-unsafe + ] [ 1 + ] bi
    ] while drop ;

Using recursion, iterating backwards:

:: (solve-1) ( accum i seq -- accum' )
    accum i [
        1 - seq [ nth-unsafe + ] 2keep (solve-1)
    ] unless-zero ;

: solve-1 ( seq -- n )
    0 swap [ length ] keep (solve-1) ;

Some test cases to confirm behavior:

{ 0 } [ { } solve-1 ] unit-test

{ 1 } [ { 1 } solve-1 ] unit-test

{ 6 } [ { 1 2 3 } solve-1 ] unit-test

Problem 2

Write a function that combines two lists by alternatively taking elements. For example: given the two lists [a, b, c] and [1, 2, 3], the function should return [a, 1, b, 2, c, 3].

We can alternately choose items from each list:

: solve-2 ( seq1 seq2 -- newseq )
    [ min-length 2 * ] 2keep '[
        [ 2/ ] [ even? ] bi _ _ ? nth-unsafe
    ] { } map-integers-as ;

Some test cases to confirm behavior:

{ { "a" 1 "b" 2 "c" 3 } } [
    { "a" "b" "c" } { 1 2 3 } solve-2
] unit-test

{ { "a" 1 "b" 2 "c" 3 } } [
    { "a" "b" "c" "d" } { 1 2 3 } solve-2
] unit-test

Problem 3

Write a function that computes the list of the first 100 Fibonacci numbers. By definition, the first two numbers in the Fibonacci sequence are 0 and 1, and each subsequent number is the sum of the previous two.

There are many approaches, including using memoization, but instead we'll just iterate from the starting values and use replicate to build up an output array.

: solve-3 ( n -- seq )
    [ 0 1 ] dip [ dup rot [ + ] keep ] replicate 2nip ;

Some test cases to confirm behavior:

{ { } } [ 0 solve-3 ] unit-test

{ { 0 } } [ 1 solve-3 ] unit-test

{ { 0 1 } } [ 2 solve-3 ] unit-test

{ { 0 1 1 2 3 5 8 13 21 34 } } [ 10 solve-3 ] unit-test

{ 573147844013817084100 } [ 100 solve-3 sum ] unit-test

Problem 4

Write a function that given a list of non negative integers, arranges them such that they form the largest possible number. For example, given [50, 2, 1, 9], the largest formed number is 95021.

We can try each-permutation of the input numbers, looking for their largest numerical value when the digits are concatenated.

: solve-4 ( seq -- n )
    0 swap [ number>string ] map
    [ concat string>number max ] each-permutation ;

Some test cases to confirm behavior:

{ 95021 } [ { 50 2 1 9 } solve-4 ] unit-test

{ 5523 } [ { 52 5 3 } solve-4 ] unit-test

Problem 5

Write a program that outputs all possibilities to put + or - or nothing between the numbers 1, 2, ..., 9 (in this order) such that the result is always 100. For example: 1 + 2 + 34 – 5 + 67 – 8 + 9 = 100.

This one is more complicated than the previous ones, but we can build it up piece by piece, using a test-case on each step to show how it works.

First, we want a word to interleave numbers amongst operators using solve-2.

: insert-numbers ( operators -- seq )
    [ length [1..b] ] [ solve-2 ] [ length 1 + suffix ] tri ;

{ { 1 f 2 + 3 f 4 } } [ { f + f } insert-numbers ] unit-test

Next, we want a word that will join adjacent digits — separated by f:

GENERIC: digits, ( prev intermediate -- next )
M: number digits, [ 10 * ] [ + ] bi* ;
M: object digits, [ [ , 0 ] dip , ] when* ;

: join-digits ( seq -- seq )
    [ [ ] [ digits, ] map-reduce , ] { } make ;

{ { 12 + 34 } } [ { 1 f 2 + 3 f 4 } join-digits ] unit-test

Since Factor is a kind of Reverse Polish notation, we'll want to swap from infix to postfix:

: swap-operators ( seq -- seq )
    dup rest-slice 2 <groups> [ 0 1 rot exchange ] each ;

{ { 12 34 + } } [ { 12 + 34 } swap-operators ] unit-test

The solution, then, is to use all-selections of addition, subtraction, and adjacency — interleaving the numbers, joining adjacent digits, swapping operators, and then calling each sequence as a quotation, filtering for the ones that return 100:

: solve-5 ( -- solutions )
    { + - f } 8 all-selections
    [ insert-numbers join-digits swap-operators ] map
    [ >quotation call( -- x ) 100 = ] filter ;

We can print the formula out by swapping the operators back to infix and printing them out:

: print-formula ( solutions -- )
    [ present ] map swap-operators " " join print ;

: solve-5. ( -- )
    solve-5 [ print-formula ] each ;

Spoilers! The printed solutions:

IN: scratchpad solve-5.
1 + 2 + 3 - 4 + 5 + 6 + 78 + 9
1 + 2 + 34 - 5 + 67 - 8 + 9
1 + 23 - 4 + 5 + 6 + 78 - 9
1 + 23 - 4 + 56 + 7 + 8 + 9
12 + 3 + 4 + 5 - 6 - 7 + 89
12 + 3 - 4 + 5 + 67 + 8 + 9
12 - 3 - 4 + 5 - 6 + 7 + 89
123 + 4 - 5 + 67 - 89
123 + 45 - 67 + 8 - 9
123 - 4 - 5 - 6 - 7 + 8 - 9
123 - 45 - 67 + 89

There was a funny post on Twitter a couple of days ago about a recent event where the "Dutch government was forced to release the source code of their DigiD digital authentication iOS app" with this piece of C# code:

Some very funny discussions continued, with comments about how good or bad this code is, and how one might rewrite it in various ways. I thought it would be a fun opportunity to show a few variations of this simple function in Factor.

Implementations

A direct translation of this code, might use cond which is basically a sequence of if statements:

: get-percentage-rounds ( percentage -- str )
    {
        { [ dup 0.0 <= ] [ drop "⚪⚪⚪⚪⚪⚪⚪⚪⚪⚪" ] }
        { [ dup 0.0 0.1 between? ] [ drop "🔵⚪⚪⚪⚪⚪⚪⚪⚪⚪" ] }
        { [ dup 0.1 0.2 between? ] [ drop "🔵🔵⚪⚪⚪⚪⚪⚪⚪⚪" ] }
        { [ dup 0.2 0.3 between? ] [ drop "🔵🔵🔵⚪⚪⚪⚪⚪⚪⚪" ] }
        { [ dup 0.3 0.4 between? ] [ drop "🔵🔵🔵🔵⚪⚪⚪⚪⚪⚪" ] }
        { [ dup 0.4 0.5 between? ] [ drop "🔵🔵🔵🔵🔵⚪⚪⚪⚪⚪" ] }
        { [ dup 0.5 0.6 between? ] [ drop "🔵🔵🔵🔵🔵🔵⚪⚪⚪⚪" ] }
        { [ dup 0.6 0.7 between? ] [ drop "🔵🔵🔵🔵🔵🔵🔵⚪⚪⚪" ] }
        { [ dup 0.7 0.8 between? ] [ drop "🔵🔵🔵🔵🔵🔵🔵🔵⚪⚪" ] }
        { [ dup 0.8 0.9 between? ] [ drop "🔵🔵🔵🔵🔵🔵🔵🔵🔵⚪" ] }
        [ drop "🔵🔵🔵🔵🔵🔵🔵🔵🔵🔵" ]
    } cond ;

But since this is a series of if statements checked sequentially, you can just check the upper bounds. And since we only care about the argument for the comparison, we can use cond-case:

: get-percentage-rounds ( percentage -- str )
    {
        { [ 0.0 <= ] [ "⚪⚪⚪⚪⚪⚪⚪⚪⚪⚪" ] }
        { [ 0.1 <= ] [ "🔵⚪⚪⚪⚪⚪⚪⚪⚪⚪" ] }
        { [ 0.2 <= ] [ "🔵🔵⚪⚪⚪⚪⚪⚪⚪⚪" ] }
        { [ 0.3 <= ] [ "🔵🔵🔵⚪⚪⚪⚪⚪⚪⚪" ] }
        { [ 0.4 <= ] [ "🔵🔵🔵🔵⚪⚪⚪⚪⚪⚪" ] }
        { [ 0.5 <= ] [ "🔵🔵🔵🔵🔵⚪⚪⚪⚪⚪" ] }
        { [ 0.6 <= ] [ "🔵🔵🔵🔵🔵🔵⚪⚪⚪⚪" ] }
        { [ 0.7 <= ] [ "🔵🔵🔵🔵🔵🔵🔵⚪⚪⚪" ] }
        { [ 0.8 <= ] [ "🔵🔵🔵🔵🔵🔵🔵🔵⚪⚪" ] }
        { [ 0.9 <= ] [ "🔵🔵🔵🔵🔵🔵🔵🔵🔵⚪" ] }
        [ drop "🔵🔵🔵🔵🔵🔵🔵🔵🔵🔵" ]
    } cond-case ;

One suggestion was to generate a substring based on the input — with the somewhat negative aspect that it allocates memory for the returned string when called:

: get-percentage-rounds ( percentage -- str )
    10 * 10 swap - >integer dup 10 +
    "🔵🔵🔵🔵🔵🔵🔵🔵🔵🔵⚪⚪⚪⚪⚪⚪⚪⚪⚪⚪" subseq ;

But another way would be to just index into the possible results, using quoted words to reduce the amount of tokens involved — resulting in this fairly aesthetic result:

: get-percentage-rounds ( percentage -- str )
    10 * ceiling >integer qw{
        ⚪⚪⚪⚪⚪⚪⚪⚪⚪⚪
        🔵⚪⚪⚪⚪⚪⚪⚪⚪⚪
        🔵🔵⚪⚪⚪⚪⚪⚪⚪⚪
        🔵🔵🔵⚪⚪⚪⚪⚪⚪⚪
        🔵🔵🔵🔵⚪⚪⚪⚪⚪⚪
        🔵🔵🔵🔵🔵⚪⚪⚪⚪⚪
        🔵🔵🔵🔵🔵🔵⚪⚪⚪⚪
        🔵🔵🔵🔵🔵🔵🔵⚪⚪⚪
        🔵🔵🔵🔵🔵🔵🔵🔵⚪⚪
        🔵🔵🔵🔵🔵🔵🔵🔵🔵⚪
        🔵🔵🔵🔵🔵🔵🔵🔵🔵🔵
    } nth ;

It's always fun to see different ways to solve problems. In the Twitter thread, that includes using binary search, building the output character-by-character, generating solutions using ChatGPT, one-liners in Python, pattern matching, unit testing, and discussions of edge cases and naming conventions.

Project Gemini is a neat modern take on the Gopher protocol. You can read the Gemini FAQ or the Gemini specification to learn more details, but the home page has a nice summary:

Gemini is a new internet protocol which

• Is heavier than gopher
• Is lighter than the web
• Will not replace either
• Strives for maximum power to weight ratio
• Takes user privacy very seriously

There are some nice Gemini clients implemented in various languages, for both the command-line and with nice user interfaces. I happen to enjoy using AV-98 and Lagrange, but many others are also great.

In a similar manner to my Gopher implementation in Factor, I recently implemented the Gemini protocol as well as a Gemini server and a Gemini user interface:

Instead of going into how the protocol or the user interface is implemented, I wanted to go over the Gemini command-line interface. In the spirit of Python's cmd module, I contributed the command-loop vocabulary to support generic line-oriented command interpreters.

We start by making a sequence of commands that our Gemini interpreter will support:

CONSTANT: COMMANDS {
    T{ command
        { name "back" }
        { quot [ drop gemini-back ] }
        { help "Go back to the previous Gemini URL." }
        { abbrevs { "b" } } }
    T{ command
        { name "forward" }
        { quot [ drop gemini-forward ] }
        { help "Go forward to the next Gemini URL." }
        { abbrevs { "f" } } }
    T{ command
        { name "history" }
        { quot [ drop gemini-history ] }
        { help "Display recently viewed Gemini URLs." }
        { abbrevs { "h" "hist" } } }
    T{ command
        { name "less" }
        { quot [ drop gemini-less ] }
        { help "View the most recent Gemini URL in a pager." }
        { abbrevs { "l" } } }
    T{ command
        { name "ls" }
        { quot [ gemini-ls ] }
        { help "List the currently available links." }
        { abbrevs f } }
    T{ command
        { name "go" }
        { quot [ gemini-go ] }
        { help "Go to a Gemini URL" }
        { abbrevs { "g" } } }
    T{ command
        { name "gus" }
        { quot [ drop "gemini://gus.guru/search" gemini-go ] }
        { help "Submit a query to the GUS search engine." }
        { abbrevs f } }
    T{ command
        { name "up" }
        { quot [ drop gemini-up ] }
        { help "Go up one directory from the recent Gemini URL." }
        { abbrevs { "u" } } }
    T{ command
        { name "url" }
        { quot [ drop gemini-url ] }
        { help "Print the most recent Gemini URL." }
        { abbrevs f } }
    T{ command
        { name "reload" }
        { quot [ drop gemini-reload ] }
        { help "Reload the most recent Gemini URL." }
        { abbrevs { "r" } } }
    T{ command
        { name "root" }
        { quot [ drop gemini-root ] }
        { help "Navigate to the most recent Gemini URL's root." }
        { abbrevs f } }
    T{ command
        { name "shell" }
        { quot [ gemini-shell ] }
        { help "'cat' the most recent Gemini URL through a shell." }
        { abbrevs { "!" } } }
    T{ command
        { name "quit" }
        { quot [ drop gemini-quit ] }
        { help "Quit the program." }
        { abbrevs { "q" "exit" } } }
}

And then we define a custom command-loop that will allow us to number the links on a Gemini page, and then by typing a number we can navigate to one of the links by detecting a "missing command":

TUPLE: gemini-command-loop < command-loop ;

M: gemini-command-loop missing-command
    over string>number [ 1 - LINKS ?nth ] [ f ] if* [
        gemini-go 3drop
    ] [
        call-next-method
    ] if* ;

You can see it in action:

$ ./factor -run=gemini.cli
Welcome to Project Gemini!
GEMINI> go gemini.circumlunar.space/news/

Official Project Gemini news feed

[1] Atom feed

2023 News

[2] 2023-01-14 - Tidying up gemini.circumlunar.space user capsules
[3] 2023-01-08 - Changing DNS server

2022 News

[4] 2022-06-20 - Three years of Gemini!
[5] 2022-01-30 - Minor specification update (0.16.1)
[6] 2022-01-22 - Mailing list archives, Atom feed for official news
[7] 2022-01-16 - Mailing list downtime, official news feed

Many years ago, Andrea Ferretti created a Factor tutorial which I had written about at the time.

One of our new core developers, Raghu Ranganathan, got permission to include the tutorial in the main Factor repository, and has reformatted it and updated it for the not-yet-released version 0.99 as the Guided tour of Factor.

You can access it in a recent nightly build by doing:

IN: scratchpad "tour" help

Check it out!

Recently, Tomasz Wegrzanowski chose Factor for his 100 Languages Speedrun: Episode 71: Factor and it encouraged us to make some improvements that I wanted to describe.

Many of our users use the Factor environment through the UI developer tools or on the command-line with the listener. Another important use case is being able to eval and run scripts -- and this is where much of Tomasz' criticism was focused.

We now do command-line eval and run scripts with auto-use? enabled. This will be available in the nightly builds and as part of an upcoming 0.99 release.

So this works now:

$ ./factor -e="1 2 + ."
3

$ cat foo.factor
USE: io
"Hello World" print
12

$ ./factor foo.factor
Hello World

--- Data stack:
12

Previously, the first example would error with a "No word named “+” found in current vocabulary search path" and the second example would complain that the "Quotation's stack effect does not match call site" because the script did not have a ( -- ) stack effect.

I appreciate that some users approach Factor differently than I do, and we love getting feedback. I wish we could solve the name conflict with factor(1), but that is more challenging.

We may adjust this slightly as it just landed last night, and if anyone has further suggestions, please keep them coming!

Factor is a programming language I've written about before and in the early days of Factor development I wrote a number of libraries and contributed to development. It's been a while since I've contributed but I still use Factor. The development environment has a very Smalltalk-like feel to it and it includes full documentation and browseable source code of libraries.

This post isn't about Factor the language, but is about some of the neat fun libraries that people have written that shows off the graphical development system a bit.

Minesweeper

The first example is an implementation of the game Minesweeper in Factor. A blog post by the author explains the implementation. To run it inside Factor, do the following:

"minesweeper" run

A new window will open showing the game. Help can be shown with:

"minesweeper" help

XKCD

Another fun example is displaying XKCD comics inside the Factor REPL. The implementation is explained by the author here.

USE: xkcd
latest-xkcd.
...comic displayed here...
random-xkcd.
...comic displayed here...

Wikipedia

If it seems like all the examples I'm using are from the excellent re-factor blog - well, most of them are. This blog post from re-factor shows pulling historical facts from Wikipedia:

USE: wikipedia
USE: calendar

today historical-events.
...a list of historical events from wikipedia for today...

yesterday historical-births.
...a list of historical births from wikipedia for yesterday...

5 weeks ago historical-deaths.
...a list of historical deaths from wikipedia for five weeks ago...

The items in the list are graphical elements that can be manipulated. Left clicking on the coloured words will open a URL in the default web browser. Right clicking allows you to push the element on the Factor stack and manipulate it.

The calendar vocab has a lot of interesting words that allow doing calculations like "5 weeks ago".

Hacker News

There's a hacker-news vocabulary that provides words to list current articles on the Hacker News website. Like the previous Wikipedia example, the graphical elements are clickable objects:

USE: hacker-news

hacker-news-top.
...list of top articles...

hacker-news-show.
...list articles related to showing projects...

CPU 8080 Emulator

A number of years ago I wrote a CPU 8080 emulator in Factor and used this to implement a Space Invaders Emulator and then emulators for a couple of other 8080 arcade games, Balloon Bomber and Lunar Rescue. These examples require the original arcade ROMs and instructions for using them are in the online help:

"rom.space-invaders" run
...opens in a new window...
"rom.balloon-bomber" run
...opens in a new window...
"rom.lunar-rescue" run
...opens in a new window...

"rom.space-invaders" help
...displays help...

Gopher Implementation

Another magical implementation from the re-factor blog, a Gopher server and a graphical Gopher Client. This is a video I made of the gopher client on YouTube:

I also did a video that shows some Factor development tools on the running Gopher client to show how everything is live in Factor:

And More

There's much more buried inside Factor. The list of articles and list of vocabularies from the online help is a good way to explore. This help system is also available offline in a Factor install. By default many libraries aren't loaded when Factor starts but you can force loading everything using load-all:

load-all
...all vocabs are loaded - prepare to wait for a while...
save
...saves the image so when factor is restarted the vocabs remain loaded...

The benefit of doing this while developing is all the online help, source and words are available via the inbuilt tools like "apropos", "usage", etc.

The Shen programming language has an extensible type system. Types are defined using sequent calculus and the system is powerful enough to create a variety of exotic types but it can be difficult when first starting with Shen to know how to use that power. In this post I hope to go through some basic examples of defining types in Shen without needing to know too much sequent calculus details.

For an overview of Shen there is Shen in 15 minutes and the Shen OS Kernel Manual. An interactive JavaScript REPL exists to try examples in the browser or pick on one of the existing Shen language ports. For these examples I'm using my Wasp Lisp port of Shen.

Shen is optionally typed. The type checker can be turned off and on. By default it is off and this can be seen in the Shen prompt by the presence of a '-' character:

(0-) ...shen code...

Turning type checking on is done by using (tc +). The '-' in the prompt changes to a '+' to show type checking is active. It can be turned off again with (tc -):

(0-) (tc +)
(1+) (tc -)
(2-) ...

Types in Shen are defined using datatype. The body of the datatype definition contains a series of sequent calculus rules. These rules define how an object in Shen can be proved to belong to a particular type. Rather than go through a detailed description of sequent calculus, I'm going to present common examples of types in Shen to learn by example and dive into details as needed. There's the Shen Language Book for much more detail if needed.

Records

One way of storing collections of data in Shen is to use lists or vectors. For example, given an the concept of a 'person' that has a name and age, this can be stored in a list with functions to get the relevent data:

(tc -)

(define make-person
  Name Age -> [Name Age])

(define get-name
  [Name Age] -> Name)

(define get-age
  [Name Age] -> Age)

(get-age (make-person "Person1" 42))
 => 42

In the typed subset of Shen we can define a type for this person object using datatype:

(datatype person
  N : string; A : number;
  _______________________
  [N A] : person;)

This defines one sequent calculus rule. The way to read it is starting with the code below the underscore line, followed by the code above it. In this case the rule states that if an expression matching the pattern [N A] is encountered, where N is a string and A is a number, then type that expression as person. With that rule defined, we can ask Shen if lists are of the type person:

(0+) ["Person" 42] : person
["Person1" 42] : person

(1+) ["Person1" "Person1"] : person
[error shen "type error"]

(2+) ["Person 42"]
["Person1" 42] : person

Given this person type, we might write a get-age function that is typed such that it only works on person objects as follows (The { ...} syntax in function definitions provides the expected type of the function):

(define get-age
  { person --> number }
  [N A] -> A)
[error shen "type error in rule 1 of get-age"]

Shen rejects this definition as not being type safe. The reason for this is because our datatype definition only states that [N A] is a person if N is a string and A is a number. It does not state that a person object is constructed only of a string and number. For example, we could have an additional definition as follows:

(datatype person2
  N : string; A : string;
  _______________________
  [N A] : person;)

Now we can create different types of person objects:

(0+) ["Person" 42 ] : person
["Person" 42] : person

(1+) ["Person" "young"] : person
["Person" "young"] : person

get-age is obviously badly typed in the presence of this additional type of person which is why Shen rejected it originally. To resolve this we need to tell Shen that an [N A] is a person if and only if N is a string and A is a person. This is done with what is called a 'left rule'. Such a rule defines how a person object can be deconstructed. It looks like this:

(datatype person3
  N : string, A: number >> P;
  ___________________________
  [N A] : person >> P;)

The way to read this type of rule is that, if [N A] is a person then N is a string and A is a number. With that loaded into Shen, get-age type checks:

(define get-age
   { person --> number }
   [N A] -> A)
get-age : (person --> number)

(0+) (get-age ["Person" 42])
42 : number

The need to create a left rule, dual to the right rule, is common enough that Shen has a short method of defining both in one definition. It looks like this - note the use of '=' instead of '_' in the separator line:

(datatype person
   N : string; A : number;
   =======================
   [N A] : person;)

(define get-age
   { person --> number }
   [N A] -> A)
get-age : (person --> number)

(0+) (get-age ["Person" 42])
42 : number

The above datatype is equivalent to declaring the two rules:

(datatype person
  N : string; A : number;
  _______________________
  [N A] : person;

  N : string, A: number >> P;
  ___________________________
  [N A] : person >> P;)

Controlling type checking

When progamming at the REPL of Shen it's common to create datatype definitions that are no longer needed, or part of a line of thought you don't want to pursue. Shen provides ways of excluding or including rules in the typechecker as needed. When defining a set of rules in a datatype, that datatype is given a name:

(datatype this-is-the-name
   ...
)

The rules within that definition can be removed from selection by the typechecker using preclude, which takes a list of datatype names to ignore during type checking:

(preclude [this-is-the-name])

To re-add a dataype, use include:

(include [this-is-the-name])

There is also include-all-but and preclude-all-but to include or remove all but the listed names. These commands are useful for removing definitions you no longer want to use at the REPL, but also for speeding up type checking in a given file if you know the file only uses a particular set of datatypes.

Enumerations

An example of an enumeration type would be days of the week. In an ML style language this can be done like:

datatype days =   monday | tuesday | wednesday
                | thursday | friday | saturday | sunday

In Shen this would be done using multiple sequent calculus rules.

(datatype days
    ____________
    monday : day;

    ____________
    tuesday : day;

    ____________
    wednesday : day;

    ____________
    thursday : day;

    ____________
    friday : day;

    ____________
    saturday : day;

    ____________
    sunday : day;)

Here there are no rules above the dashed underscore line, meaning that the given symbol is of the type day. A function that uses this type would look like:

(define day-number
  { day --> number }
  monday    -> 0
  tuesday   -> 1
  wednesday -> 2
  thursday  -> 3
  friday    -> 4
  saturday  -> 5
  sunday    -> 6)

It's quite verbose to define a number of enumeration types like this. It's possible to add a test above the dashed underline which allows being more concise. The test is introduced using if:

(datatype days
  if (element? Day [monday tuesday wednesday thursday friday saturday sunday])
  ____________________________________________________________________________
  Day : day;)

(0+) monday : day
monday : day

Any Shen code can be used in these test conditions. Multiple tests can be combined:

(datatype more-tests
  if (number? X)
  if (>= X 5)
  if (<= X 10)
  ___________
  X : between-5-and-10;)

  (2+) 5 : between-5-and-10
  5 : between-5-and-10

  (3+) 4 : between-5-and-10
  [error shen "type error\n"]

Polymorphic types

To create types that are polymorphic (ie. generic), like the built-in list type, include a free variable representing the type. For example, something like the built in list where the list elements are stored as pairs can be approximated with:

(datatype my-list
   _____________________
   my-nil : (my-list A);

   X : A; Y : (my-list A);
   ========================
   (@p X Y) : (my-list A);)


(define my-cons
  { A --> (my-list A) --> (my-list A) }
  X Y -> (@p X Y))

(0+) (my-cons 1 my-nil)
(@p 1 my-nil) : (my-list number)

(1+) (my-cons 1 (my-cons 2 my-nil))
(@p 1 (@p 2 my-nil)) : (my-list number)

(2+) (my-cons "a" (my-cons "b" my-nil))
(@p "a" (@p "b" my-nil)) : (my-list string)

Notice the use of the '=====' rule to combine left and right rules. This is required to enable writing something like my-car which requires proving that the type of the car of the list is of type A:

(define my-car
   { (my-list A) --> A }
   (@p X Y) -> X)

List encoded with size

Using peano numbers we can create a list where the length of the list is part of the type:

(datatype list-n
  ______
  [] : (list-n zero A);

  X : A; Y : (list-n N A);
  ================================
  [ X | Y ] : (list-n (succ N) A);)      

(define my-tail
  { (list-n (succ N) A) --> (list-n N A) }
  [Hd | Tl] -> Tl)

(define my-head
  { (list-n (succ N) A) --> A }
  [Hd | Tl] -> Hd)

This gives a typesafe head and tail operation whereby they can't be called on an empty list:

(0+) [] : (list-n zero number)
[] : (list-n zero number)

(1+) [1] : (list-n (succ zero) number)
[1] : (list-n (succ zero) number)

(2+) (my-head [])
[error shen "type error\n"]

(3+) (my-head [1])
1 : number

(4+) (my-tail [1 2 3])
[2 3] : (list-n (succ (succ zero)) number)

(5+) (my-tail [])
[error shen "type error\n"]      

Power and Responsibility

Shen gives a lot of power in creating types, but trusts you to make those types consistent. For example, the following creates an inconsistent type:

(datatype person
  N : string; A : number;
  _______________________
  [N A] : person;

  N : string; A : string;
  _______________________
  [N A] : person;

  N : string, A: number >> P;
  ___________________________
  [N A] : person >> P;)

Here we are telling Shen that a string and number in a list is a person, and so too is a string and another string. But the third rule states that given a person, that is is composed of a string and a number only. This leads to:

(0+) (get-age ["Person" "Person"])
...

This will hang for a long time as Shen attempts to resolve the error we've created.

Conclusion

Shen provides a programmable type system, but the responsibility lies on the programmer for making sure the types are consisitent. The examples given here provide a brief overview. For much more see The Book of Shen. The Shen OS Kernel Manual also gives some examples. There are posts on the Shen Mailing List that have more advanced examples of Shen types. Mark Tarver has a case study showing converting a lisp interpreter in Shen to use types.