Pyret Types Part 1: an Initial Exploration

This summer I am beginning research with a primary goal of adding a new type to the Pyret Programming Language. While I have hacked on my own programming language (Sailfish) and contributed to a paper published as part of 2022 IEEE/ACM 44th International Conference on Software Engineering (ICSE), I have yet to really contribute to a programming language.

What is Pyret?

Pyret is a programming language designed to serve as an outstanding choice for programming education while exploring the confluence of scripting and functional programming. It’s under active design and development, and free to use or modify. – pyret.org

Getting Started

The easiest way to experiment with Pyret and see the type-checker in action:

1. open your browser of choice and navigate to the CPO (code.pyret.org)
2. click Open Editor
3. write some code with annotations in the left side (definition area)

   add-and-to-string :: Number, Number -> String
   fun add-and-to-string(num-1, num-2):
    sum = num-1 + num-2
    to-string(sum)
   end
   

4. click the drop down next to run and select Type-check and run (beta)
5. click Type-check and run (beta)
6. in the interactive area (right side), type add-and-to-string(1, 10) and hit enter
7. observe "11" outputted in the console on the right
8. rewrite and introduce a bug

   add-and-to-string :: Number, String -> String
   fun add-and-to-string(num-1, num-2):
    sum = num-1 + num-2
    to-string(sum)
   end
   

9. click Type-check and run (beta) and observe the type check error

Optional Type Checking

Ultimately, Pyret is a dynamic language with annotations and an optional type checker. Thus, consider the following levels of type enforcement for a method that takes in a number and calculates the square.

Example 1: no annotations and type checker off

fun square_num(n):
  n * n
end

On execution with the wrong input type:

> square_num("10")
Evaluating this Times (*) expression errored:
  n * n
The left side was:

"10"
The right side was:

"10"
The * operator expects to be given two Numbers.

Example 2: input annotations and type checker off

fun square_num(n :: Number):
  n * n
end

On execution with the wrong input type:

> square_num("10")
The Number annotation
    fun square_num(n :: Number):
was not satisfied by the value

"10"

Example 3: input annotations and type checker on

fun square_num(n :: Number):
  n * n
end

On execution with the wrong input type:

> square_num("10")
Type checking failed because of a type inconsistency.

The type constraint Number was incompatible with the type constraint String

Example 4: full function annotations and type checker on

square_num :: Number -> Number
fun square_num(n):
  n * n
end

On execution with the wrong input type:

> square_num("10")
Type checking failed because of a type inconsistency.

The type constraint Number was incompatible with the type constraint String

Example 5: full function annotations and type checker on with incorrect function implementation

square_num :: Number -> Number
fun square_num(n):
  n * n
end

On compilation:

Type checking failed because of a type inconsistency.

The type constraint Number was incompatible with the type constraint String

Conclusion

Since type checking is off by default, unless users add type annotations, new types won’t, alter the compilation or execution process of existing Pyret programs. However, we do enable better tooling such as an improved language server (al beit the only language server is a WIP) or even filling type holes in improved REPL editors like Repartee.