Yeahhhhh, I have no idea what I'm doing here.. Haskell Functor type class in UrWeb ? .

hask_functor.ur

datatype notlist a = NotNil | NotCons of (a * notlist a)

signature NOTFUNCTOR = sig
  class notfunctor :: (Type -> Type) -> Type
  val fmap : f :: (Type -> Type) -> a ::: Type -> b ::: Type -> (a -> b) -> f a -> f b
  val mkNF : f ::: (Type -> Type) -> (a ::: Type -> b ::: Type -> (a -> b) -> f a -> f b) -> notfunctor (f)

  val notfunctor_notlist : notfunctor notlist
end

structure NotListFunctor : NOTFUNCTOR = struct
  class notfunctor

  fun fmap [_] [a] [b] (f : a -> b) (xs : notlist a) : notlist b =
      let
        fun f' ys = case ys of
                      NotNil => NotNil
                    | NotCons (hd,tl) => NotCons (f hd, f' tl)
      in
        f' xs
      end

  fun mkNF [_] g : notfunctor (notlist) = g

  val notfunctor_notlist = mkNF (fmap)
end