A non-compiling prism implementation where the applicative instance is AWOL.

prism.idr

module Optic.Prism

import Data.List
%default total

-- Const
data Const a b = Constant a

implementation Functor (Const a) where
  map _ (Constant x) = (Constant x)

implementation Monoid m => Applicative (Const m) where
  pure _ = Constant neutral
  (Constant x) <*> (Constant y) = Constant (x <+> y)

runConst : Const a b -> a
runConst (Constant x) = x

-- Prism
Prism : Type -> Type -> Type -> Type -> Type
Prism s t a b = {f : Type -> Type} -> Applicative f => (a -> f b) -> s -> f t

prism : (a -> s) -> (s -> Maybe a) -> Prism s s a a
prism encode decode fn s =
  case (decode s) of
       Nothing  => pure s
       (Just v) => map encode $ fn v

view : Prism s s a a -> s -> Maybe a
view p x = runConst $ p (Constant . Just) x

-- Maybe Prism
justPrism : Prism (Maybe a) (Maybe a) a a
justPrism = prism Just id

getNat : Maybe Nat
getNat = view justPrism (Just 1) -- Can't find applicative of f1.

If you make f explicit:

Prism : Type -> Type -> Type -> Type -> Type
Prism s t a b = (f : Type -> Type) -> Applicative f => (a -> f b) -> s -> f t

prism : (a -> s) -> (s -> Maybe a) -> Prism s s a a
prism encode decode _ _ fn s =
  case decode s of
    Nothing  => pure s
    (Just v) => map encode $ fn v

view : Prism s s a a -> s -> Maybe a
view p x = runConst $ p _ (Constant . Just) x

it seems to work.