chore: improve demo example

examples/02_demonstration/demo.midas

@@ -1,10 +1,15 @@
 predicate in_range(min: float, max: float)(v: float) = min <= v & v <= max
 predicate is_ratio = in_range(0, 1)
 
-type Money = float
+type Currency = float
-type Price[T <: Money] = T where _ >= 0
+type Price[T <: Currency] = T where _ >= 0
 
-type EUR = Money
+extend Price[T <: Currency] {
-type USD = Money
+    def __add__: fn(Price[T], /) -> Price[T]
+}
 
-type Reduction = float where is_ratio(_)
+type EUR = Currency
+type USD = Currency
+type CHF = Currency
+
+type Discount = float where is_ratio(_)

examples/02_demonstration/demo.py

@@ -1,19 +1,30 @@
 from typing import TypeVar, cast
 
-from demo_stubs import EUR, USD, Money, Price, Reduction
+from demo_stubs import CHF, EUR, USD, Currency, Price, Discount
 
-T = TypeVar("T", bound=Money)
+T = TypeVar("T", bound=Currency)
 
 
-def apply_reduction(amount: Price[T], reduction: Reduction) -> Price[T]:
+def apply_discount(amount: Price[T], discount: Discount) -> Price[T]:
-    return cast(Price[T], (1.0 - reduction) * amount)
+    return cast(Price[T], (1.0 - discount) * amount)
 
 
 a1 = cast(Price[EUR], 3.2)
 a2 = cast(Price[USD], 10.4)
-r1: Reduction = cast(Reduction, 0.2)
+r1 = cast(Discount, 0.2)
 
-print(apply_reduction(a1, r1))
+print(apply_discount(a1, r1))
-print(apply_reduction(a2, r1))
+print(apply_discount(a2, r1))
 
-# a3 = a1 + a2
+a3 = a1 + a1
+a4 = a1 + a2  # cannot add euros and dollars
+a3 = a2  # cannot change variable type
+
+dyn_price = float(input("Price (CHF): "))
+dyn_discount = float(input("Discount (0.0-1.0): "))
+discounted = apply_discount(
+    cast(Price[CHF], dyn_price),
+    cast(Discount, dyn_discount),
+)
+
+print(f"Discounted: CHF {discounted}")

examples/02_demonstration/demo_stubs.pyi

@@ -0,0 +1,14 @@
+from __future__ import annotations
+from typing import Generic, TypeVar
+
+class Currency(float): ...
+
+_T0 = TypeVar("_T0", bound=Currency, covariant=True)
+
+class Price(Currency, Generic[_T0]):
+    def __add__(self, _0: Price[_T0], /) -> Price[_T0]: ...
+
+class EUR(Currency): ...
+class USD(Currency): ...
+class CHF(Currency): ...
+class Discount(float): ...