20. Dependent Types

A dependent type is a type whose definition depends on its value. Jam only supports a subset of features usually indicated when referring to dependent types.

A set of assumptions can be applied to any value in Jam. These assumptions must hold when using the type. An assumption can be any derivative value that results in a boolean (such as a method call, or comparison).

20.1. Syntax

Assertion  ::=  "assert" Value
Assumption ::=  "assume" Value

20.1.1. Example

def sqrt(x)
  # x >= 0 must be true for this scope
  assume x >= 0

  return # sqrt implementation
end

# n doesn't have any assumptions, so it could be anything
n = input() as Int

# For sqrt(x), x must be >= 0
# Type error, n doesn't meet condition: n >= 0
puts(sqrt(n))

# Branches on a condition implicitly create assumptions
if n >= 0
  # Thus this is valid
  puts(sqrt(n))
else
  puts("n must be >= 0")
end

# Jam does not have a deep understanding
if n < 0
  puts("n is < 0")
else
  # Type error, n doesn't meet condition n >= 0
  puts(sqrt(n))
end

# Can be explicitly overridden, if required
assume n >= 0
puts(sqrt(n))

# Will fail at runtime if assertion is not met
# Thus it also implicitly creates an assumption
assert n >= 0
puts(sqrt(n))