Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- module Test(MyType,x,y,z,createMyType) where
- data MyType = MT { x :: Int, y :: Int, z :: Int }
- createMyType :: Int -> Int -> MyType
- createMyType myX myY = MT { x = myX, y = myY, z = 5 - myX - myY }
- {-# LANGUAGE GADTs, TypeFamilies, RankNTypes, StandaloneDeriving, UndecidableInstances, TypeOperators #-}
- data Z = Z
- data S n = S n
- data Nat n where
- Zero :: Nat Z
- Suc :: Nat n -> Nat (S n)
- deriving instance Show (Nat n)
- type family (:+) a b :: *
- type instance (:+) Z b = b
- type instance (:+) (S a) b = S (a :+ b)
- plus :: Nat x -> Nat y -> Nat (x :+ y)
- plus Zero y = y
- plus (Suc x) y = Suc (x `plus` y)
- type family (:*) a b :: *
- type instance (:*) Z b = Z
- type instance (:*) (S a) b = b :+ (a :* b)
- times :: Nat x -> Nat y -> Nat (x :* y)
- times Zero y = Zero
- times (Suc x) y = y `plus` (x `times` y)
- data (:==) a b where
- Refl :: a :== a
- deriving instance Show (a :== b)
- cong :: a :== b -> f a :== f b
- cong Refl = Refl
- data Triple where
- Triple :: Nat x -> Nat y -> Nat z -> (z :== (x :+ y)) -> Triple
- deriving instance Show Triple
- -- Half a decision procedure
- equal :: Nat x -> Nat y -> Maybe (x :== y)
- equal Zero Zero = Just Refl
- equal (Suc x) Zero = Nothing
- equal Zero (Suc y) = Nothing
- equal (Suc x) (Suc y) = cong `fmap` equal x y
- triple' :: Nat x -> Nat y -> Nat z -> Maybe Triple
- triple' x y z = fmap (Triple x y z) $ equal z (x `plus` y)
- toNat :: (forall n. Nat n -> r) -> Integer -> r
- toNat f n | n < 0 = error "why can't we have a natural type?"
- toNat f 0 = f Zero
- toNat f n = toNat (f . Suc) (n - 1)
- triple :: Integer -> Integer -> Integer -> Maybe Triple
- triple x y z = toNat (x' -> toNat (y' -> toNat (z' -> triple' x' y' z') z) y) x
- data Yatima where
- Yatima :: Nat x -> Nat y -> Nat z -> ((x :* x) :+ (y :* y) :+ (z :* z) :== S (S (S (S (S Z))))) -> Yatima
- deriving instance Show Yatima
- yatima' :: Nat x -> Nat y -> Nat z -> Maybe Yatima
- yatima' x y z =
- fmap (Yatima x y z) $ equal ((x `times` x) `plus` (y `times` y) `plus` (z `times` z)) (Suc (Suc (Suc (Suc (Suc Zero)))))
- yatima :: Integer -> Integer -> Integer -> Maybe Yatima
- yatima x y z = toNat (x' -> toNat (y' -> toNat (z' -> yatima' x' y' z') z) y) x
- {-
- λ> triple 3 4 5
- Nothing
- λ> triple 3 4 7
- Just (Triple (Suc (Suc (Suc Zero))) (Suc (Suc (Suc (Suc Zero)))) Refl (Suc (Suc (Suc (Suc (Suc (Suc (Suc Zero))))))))
- λ> yatima 0 1 2
- Just (Yatima Zero (Suc Zero) (Suc (Suc Zero)) Refl)
- λ> yatima 1 1 2
- Nothing
- -}
- open import Relation.Binary.PropositionalEquality (_≡_)
- open import Data.Nat (ℕ; _+_)
- open import Data.Product (Σ; ×; _,_)
- FiveTriple : Set
- FiveTriple = Σ (ℕ × ℕ × ℕ) (λ{ (x , y , z) → x + y + z ≡ 5 })
- someFiveTriple : FiveTriple
- someFiveTriple = (0 , 2 , 5) , refl
- data MyType = MT {x :: Int, y :: Int, z :: Int } deriving Show
- createMyType :: Int -> Int -> Int -> Maybe MyType
- createMyType a b c
- | a + b + c == 5 = Just MT { x = a, y = b, z = c }
- | otherwise = Nothing
Add Comment
Please, Sign In to add comment