All the polymorphism in Idris 2

example.idr

f : {a : Type} -> a -> a
f {a=Int}    x = 2 * x
f {a=String} x = "twice " ++ x
f {a=_}      x = x

main : IO ()
main = do
  -- Ad-hoc polymorphism type 1: type-based overloading
  -- Also in: C++, Java
  printLn $ "hi " ++ "there" -- uses the ++ for String
  printLn $ [1,2] ++ [3,4,5] -- uses the ++ for List Int

  -- Ad-hoc polymorphism type 2: typeclasses
  -- Also in: Haskell, Rust
  printLn $ the Nat $ 5 + 5 -- uses the Nat typeclass instance
  printLn $ the Int $ 5 + 5 -- uses the Int typeclass instance

  -- Parametric polymorphism type 1: free theorems
  -- Also in: ML, Haskell
  printLn $ id "hi there!" -- instantiates id for String
  printLn $ id (the Int 5) -- instantiates id for Int

  -- Parametric polymorphism type 2: no free theorems
  -- Also in: C++, Odin
  printLn $ f "seventeeen" -- calls f {String}
  printLn $ f (the Int 17) -- calls f {Int}

  -- TODO: also elaborator reflection
  -- Not sure what other language feature this best compares to