Fixed size list signatures in htdp/isl+

General
1

I wanted to try one of the exercises from

6 Functional Abstraction

using signatures instead of contracts, but I hit what seems to be a
limitation of the signatures in ISL+. In particular there seems to be no
way to express a list of a fixed number of elements, which is used in
Exercise 26. I realize the exercise could be updated to use structs
instead, but fixed sized lists seem like a popular idea in "beginner
code". Does it make sense to add something like (List a b c) to
signatures (in the style of typed/racket), or is it better to discourage
this style in the teaching languages?

2 
#lang htdp/asl

(define fixed-size? (signature (predicate (λ (x) (= (length x) 3)))))

(: f [(combined (ListOf Integer) fixed-size?) -> Natural])
(define (f x) 2)

(f '[3 2 1])
2 Likes
3

EmEf via Racket Discourse notifications@racket.discoursemail.com
writes:

#lang htdp/asl

(define fixed-size? (signature (predicate (λ (x) (= (length x) 3)))))

(: f [(combined (ListOf Integer) fixed-size?) -> Natural])
(define (f x) 2)

(f '[3 2 1])

Thank you, that is indeed a viable approach to fixing the list
length. Your answer also helped me realize that structs are really a
better answer for the original exercise, since it is not just the length
of the list but also the type of the first element and the type of the
second element that matter. So some "match-like" specification would
work (if it existed), but just specifying the length is not enough.

David

4

*sl is designed to support principles of systematic program design that work in the absence of match like constructs in the languages students will encounter. Part of the goal is to develop the mental discipline to cope with absence of static checking, whether this means no type system at all — say in Python (please don’t mention it’s type hints) — or a (n HM) type (inference) system such as ML’s or Haskell’s. All of them come with gaps, meaning conditions that are (at best) checked at run time.

If the workd had only (Typed) Racket-like languages, *sl would look very different.

Adding checked signatures is a compromise that we will explore at Northeastern this coming semester.