SHARE
TWEET

Untitled

a guest Dec 3rd, 2019 85 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. module Main
  2.  
  3. nat2type : Bool -> Type
  4. nat2type False = Integer
  5. nat2type True = List Integer    
  6.  
  7. hello : (f: Bool) -> nat2type f          
  8. hello False = 10                            
  9. hello True = [10, 20]  
  10.  
  11. -- How do I implement 'printany' ??
  12. -- It currently fails at typecheck
  13. --
  14. -- When checking an application of function Prelude.Monad.>>=:
  15. --        Can't find implementation for Show (nat2type f)
  16. --
  17. -- Moreover, how do I consume an induced type?  
  18. printany : Show a => a -> IO ()                        
  19. printany a = print a                                    
  20.                                                        
  21. main : IO ()                                  
  22. main = do
  23.     putStrLn "Hello World"
  24.     v <- getLine
  25.     let f = if v == "True" then True else False  
  26.     let result = hello f  
  27.     printany result
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top