fork(1) download
copy 
  1. {-# LANGUAGE GADTs, KindSignatures, DataKinds, PolyKinds, RankNTypes, TypeOperators #-}
  2.  
  3. import Data.Either
  4. import Data.Functor
  5. import Control.Monad
  6.  
  7. data Nat = Z | S Nat
  8.  
  9. data Natty :: Nat -> * where
  10. 	Zy :: Natty Z
  11. 	Sy :: Natty n -> Natty (S n)
  12.  
  13. data Finny :: Nat -> Nat -> * where
  14. 	FZ :: Finny (S n) Z
  15. 	FS :: Finny n m -> Finny (S n) (S m)
  16.  
  17. type Finny0 n = Finny (S n)
  18.  
  19. data Vec :: * -> Nat -> * where
  20.   VNil :: Vec a Z
  21.   VCons :: a -> Vec a n -> Vec a (S n) 
  22.  
  23. fromIntNatty :: Int -> (forall n. Natty n -> b) -> b
  24. fromIntNatty 0 f = f Zy
  25. fromIntNatty n f = fromIntNatty (n - 1) (f . Sy)
  26.  
  27. fromNattyFinny0 :: Natty n -> (forall m. Finny0 n m -> b) -> b
  28. fromNattyFinny0  Zy    f = f FZ
  29. fromNattyFinny0 (Sy n) f = fromNattyFinny0 n (f . FS)
  30.  
  31. fromIntNattyFinny0 :: Int -> (forall n m. Natty n -> Finny0 n m -> b) -> b
  32. fromIntNattyFinny0 n f = fromIntNatty n $ \n'' -> fromNattyFinny0 n'' (f n'')
  33.  
  34. vfromList :: [a] -> (forall n. Vec a n -> b) -> b
  35. vfromList    []  f = f VNil
  36. vfromList (x:xs) f = vfromList xs (f . VCons x)
  37.  
  38. vhead :: Vec a (S n) -> a
  39. vhead (VCons x xs) = x
  40.  
  41. vtoList :: Vec a n -> [a]
  42. vtoList  VNil        = []
  43. vtoList (VCons x xs) = x : vtoList xs
  44.  
  45. vlength :: Vec a n -> Natty n
  46. vlength  VNil        = Zy
  47. vlength (VCons x xs) = Sy (vlength xs)
  48.  
  49. vlookup :: Finny n m -> Vec a n -> a
  50. vlookup  FZ    (VCons x xs) = x
  51. vlookup (FS i) (VCons x xs) = vlookup i xs
  52.  
  53. vtake :: Finny0 n m -> Vec a n -> Vec a m
  54. vtake  FZ     _           = VNil
  55. vtake (FS i) (VCons x xs) = VCons x (vtake i xs)
  56.  
  57. data (:<=) :: Nat -> Nat -> * where
  58. 	Z_le_Z :: Z :<= m
  59. 	S_le_S :: n :<= m -> S n :<= S m
  60.  
  61. type n :< m = S n :<= m
  62.  
  63. (<=?) :: Natty n -> Natty m -> Either (m :< n) (n :<= m)
  64. Zy   <=? m    = Right Z_le_Z
  65. Sy n <=? Zy   = Left (S_le_S Z_le_Z)
  66. Sy n <=? Sy m = either (Left . S_le_S) (Right . S_le_S) $ n <=? m
  67.  
  68. inject0Le :: Finny0 n p -> n :<= m -> Finny0 m p
  69. inject0Le  FZ     _          = FZ
  70. inject0Le (FS i) (S_le_S le) = FS (inject0Le i le)
  71.  
  72. main = do
  73. 	xs <- readLn :: IO [Int]
  74. 	ns <- read <$> getLine
  75. 	forM_ ns $ \n -> putStrLn $
  76. 		fromIntNattyFinny0 n $ \n' i' ->
  77. 		vfromList xs         $ \xs'   ->
  78. 		case n' <=? vlength xs' of
  79. 			Left  _  -> "What should I do with this input?"
  80. 			Right le -> show $ vtoList $ vtake (inject0Le i' le) xs'
Success #stdin #stdout 0s 4620KB
comments ()
stdin
copy 
[1,2,3,4,5,6]
[0,2,5,6,7,10]
stdout
copy 
[]
[1,2]
[1,2,3,4,5]
[1,2,3,4,5,6]
What should I do with this input?
What should I do with this input?
https://ideone.com/3GX0hd
language:
Haskell (ghc 8.4.4)
created:
10 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!