Joris KBos's questions

Estou bastante confortável com o Agda. Decidi experimentar o Lean, mas acho que a igualdade proposicional está realmente me atrapalhando. Às vezes, acho que o RFL simplesmente funciona, mas outras vezes não, por razões que me escapam completamente, o que é bastante frustrante. Para dar um exemplo:

inductive Λ where
  | var : String → Λ
  | app : Λ → Λ → Λ
  | abs : String → Λ → Λ
  deriving Repr, BEq, DecidableEq

def FV : Λ → HashSet String
  | Λ.var x => HashSet.ofList [x]
  | Λ.app m n  => FV m ∪ FV n
  | Λ.abs x m => (FV m).erase x
  
#eval FV (Λ.var "x")  -- Std.HashSet.ofList ["x"]
example : FV (Λ.var "x") = HashSet.ofList ["x"] := rfl  -- fine
example : (2 == 1 + 1) = true := rfl -- fine
#eval FV (Λ.var "x") == HashSet.ofList ["x"]  -- true
example : (FV (Λ.var "x") == HashSet.ofList ["x"]) = true := rfl
--type mismatch
--  rfl
--has type
--  ?m.9390 = ?m.9390 : Prop
--but is expected to have type
--  (FV (Λ.var "x") == HashSet.ofList ["x"]) = true : Prop

As expressões são avaliadas conforme o esperado, mas nos dois primeiros exemplos, rfl funciona perfeitamente, mas no último, misteriosamente, não funciona, aparentemente sem reduzir os termos em ambos os lados de = . Eu poderia imaginar dois HashSets com os mesmos valores nem sempre sendo iguais, pois poderiam ter acabado em grupos diferentes, mas não tenho certeza se esse é o problema, porque parece ser avaliado perfeitamente.

Em Haskell, costumo usar liftA2 em funções como o combinador S'. Isso funciona porque o Haskell STL instancia Functor e Applicative para funções (consulte https://hackage.haskell.org/package/base-4.12.0.0/docs/src/GHC.Base.html#line-818). Pelo que pude descobrir, o Idris STL não faz isso (além do fato de que também não consegui encontrar o liftA2 no STL), então pensei em fazer isso sozinho. Só que parece não funcionar, mas talvez eu não conheça Idris bem o suficiente, pois só tentei hoje.

Eu sou capaz de instanciar Functor e Applicative para \b => a -> b, mas o sistema de tipos não parece capaz de descobrir que quando eu uso algo do tipo a -> b, o functor do aplicativo deve ser \b => uma -> b.

Eu tenho o seguinte código:

Functor (\b => a -> b) where
  map = (.)

Applicative (\b => a -> b) where
  pure = const
  (<*>) f g x = f x (g x)

liftA2 : (Functor f, Applicative f) => (a -> b -> c) -> f a -> f b -> f c
liftA2 = (<*>) .: map

S' : (b -> c -> d) -> (a -> b) -> (a -> c) -> a -> d
S' = liftA2

Mas a definição de S' dá o seguinte erro:

Error: While processing right hand side of S'. Can't find an implementation for (Functor ?f, Applicative ?f).

Helpers:16:6--16:12
 12 | liftA2 : (Functor f, Applicative f) => (a -> b -> c) -> f a -> f b -> f c
 13 | liftA2 = (<*>) .: map
 14 |
 15 | S' : (b -> c -> d) -> (a -> b) -> (a -> c) -> a -> d
 16 | S' = liftA2
           ^^^^^^