Idris-dev
Idris-dev copied to clipboard
Can't find implementation
The program
> import Data.List
> %default total
> %auto_implicits off
> %access public export
> NaturalTransformation : {F, G : Type -> Type} ->
> (Functor F, Functor G) =>
> ({T : Type} -> F T -> G T) -> Type
>
> NaturalTransformation {F} h = {X, Y : Type} -> (f : X -> Y) -> (fx : F X) ->
> (map f . h) fx = (h . map f) fx
> listToMaybe_NaturalTransformation : NaturalTransformation {F = List} {G = Maybe} listToMaybe
> listToMaybe_NaturalTransformation f Nil = Refl
> listToMaybe_NaturalTransformation f (x :: xs) = Refl
> using (F : Type -> Type)
> implementation [FunctorComposition] Functor F => Functor (F . F) where
> map = map . map
> using implementation FunctorComposition
> joinNaturalTransformation : NaturalTransformation {F = List . List} {G = List} join
fails to type check with
- + Errors (1)
`-- ./Monad/issue.lidr line 23 col 30:
When checking type of Main.joinNaturalTransformation:
Can't find implementation for Functor (List . List)
Is this the expected behavior? How can one state that join
for lists is a natural transformation in Idris?