# Statements of "this implies that" or "if this then that" are
# essential to proofs.  Functions from type X to type Y are
# ubiquitous in programs.  These are corresponding constructs.

((("abc":String) (string_length : String -> Integer) : Integer) trace (\@t->t))

# The expression of interest is
#   ((("abc":String) (string_length : String -> Integer) : Integer)
# It would work just as well without the type annotations as
#   ("abc" string_length)
# because Ambidexter can infer types automatically.
# Read the expression both as a proof and as a program.
#    As a proof it is modus ponens with the premises reversed.
#          String              second premise
#          String -> Integer   first premise
#          -----------------
#          Integer             conclusion
#
#    String -> Integer as a logical proposition means
#    "If String then Integer."
#    It may also be read as "String implies Integer".
#    As a programming type "String -> Integer" means
#    "function taking a String argument and returning an Integer".
#
#    As a program:
#          Take the String value "abc"
#          and apply the function string_length to it.
#          The composite expression
#                "abc" string_length
#          has type Integer.

# Notice that in this program we have "trace (\@t->t)" rather than be.
# It similarly forms a program based on the expression.
# In this case it says to observe the expression.