fork download
copy 
  1. {-# LANGUAGE GADTs, Rank2Types #-}
  2. import Prelude hiding (Ordering, Eq, compare, length, (!!))
  3.  
  4. data Z = Z
  5. data S n = S n
  6.  
  7. data LT = LT
  8. data GT = GT
  9. data EQ = EQ
  10.  
  11. data Ordering n m o where
  12.   EqZ :: Ordering Z Z EQ
  13.   EqS :: (Nat n, Nat m) => Ordering n m EQ -> Ordering (S n) (S m) EQ
  14.   LtZ :: Nat m => S m -> Ordering Z (S m) LT
  15.   LtS :: (Nat n, Nat m) => Ordering n m LT -> Ordering (S n) (S m) LT
  16.   GtZ :: Nat n => S n -> Ordering (S n) Z GT
  17.   GtS :: (Nat n, Nat m) => Ordering n m GT -> Ordering (S n) (S m) GT
  18. data SomeOrdering n m = forall o. SomeOrdering (Ordering n m o)
  19.  
  20. data IsZero n where
  21.   IsZero :: IsZero Z
  22.   NotZero :: Nat n => S n -> IsZero (S n)
  23.  
  24. class Nat n where
  25.   toInt :: n -> Int
  26.   isZero :: n -> IsZero n
  27.   compare :: Nat m => n -> m -> SomeOrdering n m
  28.  
  29. instance Nat Z where
  30.   toInt _ = 0
  31.   isZero _ = IsZero
  32.   compare _ m =
  33.     case isZero m of
  34.       IsZero -> SomeOrdering EqZ
  35.       NotZero _ -> SomeOrdering $ LtZ m
  36. instance Nat n => Nat (S n) where
  37.   toInt ~(S n) = 1 + toInt n
  38.   isZero n = NotZero n
  39.   compare ~(S n) m =
  40.     case isZero m of
  41.       IsZero -> SomeOrdering $ GtZ (S n)
  42.       NotZero ~(S m') ->
  43.         case compare n m' of
  44.           SomeOrdering o@(LtZ _) -> SomeOrdering (LtS o)
  45.           SomeOrdering o@(LtS _) -> SomeOrdering (LtS o)
  46.           SomeOrdering o@(GtZ _) -> SomeOrdering (GtS o)
  47.           SomeOrdering o@(GtS _) -> SomeOrdering (GtS o)
  48.           SomeOrdering EqZ -> SomeOrdering (EqS EqZ)
  49.           SomeOrdering o@(EqS _) -> SomeOrdering (EqS o)
  50.  
  51. reifyInt :: Int -> (forall n. Nat n => n -> a) -> a
  52. reifyInt 0 k = k Z
  53. reifyInt n k = reifyInt (n-1) $ \m -> k (S m)
  54.  
  55. data Vec n a where
  56.   Nil :: Vec Z a
  57.   (:::) :: Nat n => a -> Vec n a -> Vec (S n) a
  58.  
  59. toList :: Vec n a -> [a]
  60. toList Nil = []
  61. toList (x ::: xs) = x : toList xs
  62.  
  63. fromList :: [a] -> (forall n. Nat n => Vec n a -> b) -> b
  64. fromList [] k = k Nil
  65. fromList (x:xs) k = fromList xs $ \xs' -> k (x ::: xs')
  66.  
  67. length :: Vec n a -> n
  68. length Nil = Z
  69. length (_ ::: xs) = S (length xs)
  70.  
  71. (!!) :: (Nat n, Nat m) => Vec m a -> Ordering n m LT -> a
  72. (x ::: _) !! (LtZ _) = x
  73. (_ ::: xs) !! (LtS o) = xs !! o
  74. _ !! _ = error "should not happen!"
  75.  
  76. main :: IO ()
  77. main = do
  78.   xs <- readLn :: IO [Int]
  79.   x <- readLn :: IO Int
  80.   reifyInt x $ \n -> fromList xs $ \ls ->
  81.     case compare n (length ls) of
  82.       SomeOrdering o@(LtZ _) -> print $ ls !! o
  83.       SomeOrdering o@(LtS _) -> print $ ls !! o
  84.       _ -> putStrLn "out of range!"
  85.  
stdin
copy 
[0,1,2,3]
3
compilation info 
[1 of 1] Compiling Main             ( prog.hs, prog.o )
Linking prog ...
stdout
copy 
3
https://ideone.com/Bi7vR
language:
Haskell (ghc 8.4.4)
created:
12 years ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!