Typed: Libraries and Utilities

This package contains a set of typed libraries. It is still under development.

1 util

(require (planet dvanhorn/typed:1:5/util))

cast : (All (T) ((Any -> Boolean : T) Any -> T))

Cast the given value to the type described by the predicate. Note the predicate must be symmetric. The cast will fail at run-time if the value does not satisfy the predicate.

Casting is useful to embed type refinements the programmer can prove that Typed Scheme is not able to reason about.

Examples:
  > (sin pi)
  - : Number
  1.2246467991473532e-16
  > (cast real? (sin pi))
  - : Real
  1.2246467991473532e-16
  > (cast string? 5)
  Cast failed

exact-round : (Real -> Integer)

exact-floor : (Real -> Integer)

exact-ceiling : (Real -> Integer)

exact-truncate : (Real -> Integer)

These operations coerce their result to exact integers.

Examples:
  > (round 3/2)
  - : Real
  2
  > (exact-round 3/2)
  - : Integer
  2
  > (round 2.5)
  - : Real
  2.0
  > (exact-round 2.5)
  - : Integer
  2

It is a contract violation to apply these operations to a non-rational real (i.e., +inf.0, -inf.0, or +nan.0), since there is no exact representation of these values.

Examples:
  > (round +inf.0)
  - : Real
  +inf.0
  > (exact-round +inf.0)
  /Users/dvanhorn/Documents/planet/typed/private/util.ss:2.19:

    (file

  /Users/dvanhorn/Documents/planet/typed/util.ss)
   broke the
  contract (-> rational? any/c) on exact-round; expected
  <rational?>, given: +inf.0

2 list

(require (planet dvanhorn/typed:1:5/list))

remf : (All (X) ((X -> Boolean) [Listof X] -> [Listof X]))

Remove the first element satisfying the given predicate (if any).

Example:
  > (remf even? '(1 3 2 5 4))
  - : (Listof Exact-Positive-Integer)
  (1 3 5 4)

interleave : (All (X) (X [Listof X] -> [Listof X]))

Interleave given element between each pair of elements in list.

Examples:
  > (interleave '* '())
  - : (Listof '*)
  ()
  > (interleave '* '(x y z))
  - : (Listof (U '* 'x 'y 'z))
  (x * y * z)

replace-at : (All (X) ([Listof X] X Nat -> [Listof X]))

remove-at : (All (X) ([Listof X] Nat -> [Listof X]))

Examples:

> (replace-at '("a" "b" "c") "z" 1)

- : (Listof String)

("a" "z" "c")

> (remove-at '("a" "b" "c") 1)

- : (Listof String)

("a" "c")

all-but-last : (All (X) ((Pair X (Listof X)) -> (Listof X)))

Given a non-empty list, returns a list of all but the last element.

Examples:
  > (all-but-last '(x))
  - : (Listof 'x)
  ()
  > (all-but-last '(x y z))
  - : (Listof (U 'x 'y 'z))
  (x y)

3 lang/posn

(require (planet dvanhorn/typed:1:5/lang/posn))

This module provides a typed variant of the lang/posn library.

Posn

A Posn is a (make-posn Integer Integer).

make-posn : (Integer Integer -> Posn)

posn? : (Any -> Boolean : Posn)

posn-x : (Posn -> Integer)

posn-y : (Posn -> Integer)

Posn constructor, predicate, and accessors.

4 2htdp/image

(require (planet dvanhorn/typed:1:5/2htdp/image))

This module provides a typed variant of the 2htdp/image library.

Base types.

Image, Color, and Pen are opaque types with predicates image?, color?, and pen?, respectively.

Angle is a synonym for Real and Nat for Exact-Nonnegative-Integer.

Image-Color is (U Color String Symbol) and the image-color? procedure is its predicate.

Mode is (U 'solid "solid" 'outline "outline") and the mode? procedure is its predicate.

Example:
  > (cast mode? "outline")
  - : Mode
  "outline"

X-Place is (U 'left 'right 'middle 'center "left" "right" "middle" "center") and the x-place? procedure is its predicate.

Example:
  > (cast x-place? "left")
  - : X-Place
  "left"

Y-Place is (U 'top 'bottom 'middle 'center 'baseline "top" "bottom" "middle" "center" "baseline") and the y-place? procedure is its predicate.

Example:
  > (cast y-place? "baseline")
  - : Y-Place
  "baseline"

Pen-Style is (U "solid" 'solid "dot" 'dot "long-dash" 'long-dash "short-dash" 'short-dash "dot-dash" 'dot-dash) and the pen-style? procedure is its predicate.