Functions can be lazy based on computations

computed_lazyness.idr

module Main

pl : Bool -> Type -> Type
pl True t = Lazy t 
pl False t = t 

-- Only defined for True.
partial
onlyTrue : Bool -> Bool
onlyTrue True = True

strictAnd : Bool -> pl False Bool -> Bool
strictAnd True b = b 
strictAnd False _ = False

lazyAnd : Bool -> pl True Bool -> Bool
lazyAnd True b = b 
lazyAnd False _ = False

-- If you type more than 2 characters and press enter the program crashes.
-- If you replace lazyAnd with strictAnd it crashes regardless of the number of
-- characters.
main : IO ()
main = do
  l <- getLine
  if lazyAnd (length l > 2) (onlyTrue False)
     then putStrLn "A"
     else putStrLn "B"