Hacker News new | past | comments | ask | show | jobs | submit login

    add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat
    add x y = x + y

Actually, (GHC) Haskell can express something like this type if you turn on the required extensions.

    data Nat = Z | S Z deriving (Eq, Ord, Show)
    data SNat (n :: Nat) where
        SZ :: SNat Z
        SS :: SNat n -> SNat (S n)

    type family Compare (a :: Nat) (b :: Nat) :: Ordering where
      Compare Z Z = EQ
      Compare (S a) Z = GT
      Compare Z (S a) = LT
      Compare (S a) (S b) = Compare a b
    
    type a < b = Compare a b ~ LT

    type family (+) (a :: Nat) (b :: Nat) :: Nat where
      Z + a = a
      a + Z = a
      (S a) + b = S (a + b)
    
    add :: (a < b) => SNat a -> SNat b -> SNat (a+b)
    add = ...



Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: