Dynamic Supertypes

For every subtype realtion. P <: Q, there is an implied conversion function of type P -> Q. This conversion does not need to be injective, nor does there need to be "retraction" function of type Q -> Maybe P.

But sometimes, this retraction does exist. Pinafore provides a general mechanism for making use of them.

Every ambipolar type T has an ambipolar greatest dynamic supertype D(T):

• D(Integer) = Number
• D(Rational) = Number
• D(T) = DynamicEntity for dynamic entity types (the main use case)
• D(T) = T for all other types

In each case, there is a "check" function that can convert D(T) back to Maybe T.

Type Pattern

If pat is a pattern of type T, then (pat: T) is a pattern of type D(T). Here's an example:

showNumberType: Number -> Text;
showNumberType n =
    case n of
        (i: Integer) -> "integer: " <> toText i;
        (r: Rational) -> "rational: " <> toText r;
        _ -> "number: " <> toText n;
    end

Check

check is simply the retraction function.

check @T: D(T) -> Maybe T

This is equivalent to

\d -> case d of (t:T) -> Just t; _ -> Nothing end

Coerce

If you're sure that the retraction will always succeed, you can use coerce. (If it doesn't, you'll get a run-time error.)

coerce @T: D(T) -> T

This is equivalent to

\d -> case d of (t:T) -> t; _ -> error "coercion from D(T) to T failed" end