Using Named Instances in Idris

named_instances.idr

class Foo (a : Type) where
  foo : List a

instance Foo Integer where
  foo = replicate 10 0

instance [ones] Foo Integer where
  foo = replicate 10 1
  
sum' : Num a => {default %instance i: Foo a} -> a
sum' = sum foo 

res : Num a => {default %instance i: Foo a} -> a
res = sum' + sum'

res_ones : Integer
res_ones = res {i=ones}

{-
Examples: 

  Idris> res
  0 : Integer
  Idris> res {i=ones}
  20 : Integer
  Idris> res_ones
  20 : Integer
-}

ex : {default %instance i : Semigroup (Maybe String)} -> Maybe String
ex = foldr (<+>) neutral [Just "sss", Just "zzz"]

ex' : {default %instance i : Semigroup (Maybe String)} -> Maybe String
ex' = concat [Just "sss", Just "zzz"]

{-
Examples:
  Idris> ex
  Just "sss" : Maybe String
  Idris> ex {i=collectJust}
  Just "ssszzz" : Maybe String
  Idris> ex'
  Just "sss" : Maybe String
  
But still:
  Idris> ex' {i=collectJust}
  Just "sss" : Maybe String
-}