Dependent Types Demo Code

demo.idr

import Data.Fin
import Data.So

-- %default total
















-- Totality
add : Int -> Int -> Int
add x y = x + y













data Sum : Int -> Type where
    MkSum1 : (a: Int) -> Sum a
    MkSum2 : (a: Int) -> (b: Int) -> Sum (a + b)
    MkSum3 : (a: Int) -> (b: Int) -> (c: Int) -> Sum (a + b + c)


sumSum : Sum a -> Sum b -> Sum (a + b)
sumSum {a} {b} _ _ = MkSum1 (a + b)









data Point : (x: Double) -> (y: Double) -> Type where
    MkPoint : (x: Double) -> (y: Double) -> Point x y


-- y = mx + b
calcM : Double -> Double -> Double -> Double -> Double
calcM x1 y1 x2 y2 = (y1 - y2) / (x1 - x2)

calcB : Double -> Double -> Double -> Double -> Double
calcB x1 y1 x2 y2 = -1 * (((calcM x1 y1 x2 y2) * x1) - y1)


-- Line Equation: y = mx + b
data Line : (m: Double) -> (b: Double) -> Type where
    MkLineFromPoints : Point x1 y1 -> Point x2 y2 -> Line (calcM x1 y1 x2 y2) (calcB x1 y1 x2 y2)
    MkLine : (m: Double) -> (b: Double) -> Line m b





isPointOnLine : Line m b -> Point x y -> Bool
isPointOnLine {m} {b} {x} {y} _ _ = ((m * x) + b) == y



data PointOnLine : Line m b -> Point x y -> Type where
    MkPointOnLine : (l: Line m b) -> (p: Point x y) -> {auto pr: m * x + b = y} -> PointOnLine l p









-- So
-- https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/So.idr



data BoundInt : Int -> Int -> Type where
    MkBoundInt : (lower: Int)
              -> (upper: Int)
              -> (value: Int)
              -> { auto pr: So (value >= lower && value <= upper) }
              -> BoundInt lower upper

















-- Natural Number Type
-- data Nat = Z | S Nat




data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] y = y
append (x :: z) y = x :: append z y









data Account : Int -> Type where
    MkAccount : (bal: Int) -> Account bal

debit : Account bal -> (x: Int) -> {auto pr: So (x <= bal)} -> Account (bal - x)
debit (MkAccount bal) x {pr} = MkAccount (bal - x)

credit : Account bal -> (x: Int) -> Account (bal + x)
credit (MkAccount bal) x = MkAccount (bal + x)

-- (((((MkAccount 22) `debit` 19) `debit` 3) `credit` 17) `debit` 12)












implementation Show (Account bal) where
    show (MkAccount bal) = "Account(balance: " ++ (show bal) ++ ")"


main : IO ()
main = do
  putStr "balance: "
  l1 <- getLine
  putStr "to debit: "
  l2 <- getLine

  let balance : Int = cast l1
  let account = MkAccount balance
  let toDebit : Int = cast l2

  -- Won't compile
--   printLn $ show $ debit account toDebit

  -- WILL compile
  case (account) of
    MkAccount bal => case (choose(toDebit <= bal)) of
        Left  p    => printLn $ show $ debit account toDebit
        Right notP => printLn $ show "Not enough funds!"

demo.java

class MyClass {
  public static Integer add(Integer x, Integer y) {
    return x + y;
  }
}






@Value
@AllArgsConstructor(access = AccessLevel.PRIVATE)
public class PosMoney {

  @NonNull private BigDecimal amountMicros;

  /* "Constructor" */
  public static Optional<PosMoney> of(BigDecimal amountMicros) {
    return Optional.ofNullable(amountMicros)
      .filter(a -> a > 0)
      .map(PosMoney::new);

  }
}









@Value
@AllArgsConstructor(access = AccessLevel.PRIVATE)
public class NonEmptyList<T> {

  @NonNull private List<T> list;

  public NonEmptyList<T> add(List<T> nums) {
    return new NonEmptyList(list.addAll(nums));
  }

  public T head() {
    /* This is safe, and will never return null */
    return list.get(0);
  }

  /* "Constructor" */
  public static <T> Optional<NonEmptyList<T>> of(List<T> nums) {
    return Optional.ofNullable(nums)
      .filter(a -> a.length() > 0)
      .map(NonEmptyList::new);
  }
}











enum Color { RED, GREEN, BLUE; }

@Value
@AllArgsConstructor(access = AccessLevel.PRIVATE)
public class NonRedColor {

  @NonNull private Color color;

  /* "Constructor" */
  public static <T> Optional<ValidColor> of(Color color) {
    return Optional.ofNullable(color)
      .filter(a -> a != RED)
      .map(NonRedColor::new);
  }
}