[Haskell-cafe] Translating a pre-image witness from agda to haskell

[Ruben Astudillo]

Dear list

     I've been playing with agda lately, I've been following the
tutorials on their homepage to get a grasp of dependent types. The
exposition has been good and clear. Some techniques can be passed over
to haskell by using GADTs and DataKinds. Some examples require
singletons to have the same kind of quantification as in agda. Currently
I am trying to write in haskell the following data type and function

    data Image {A B : Set} (f : A -> B) : B -> Set where
      im : (x : A) -> Image f (f x)

    inv : {A B : Set} (f : A -> B) (y : B) -> Image f y -> A
    inv f .(f x) (im x) = x

The `Image` datatype correspond to the proposition that the function `f
: A -> B` has a pre-image for certain element on `B`. This is witnessed
only if the `im` data constructor exists. The `inv` function is there
only to show how agda can know by the presence of the `im x` data
constructor that the value of `y` cannot be other than `f x`, mind
bending stuff.

     I've been trying to write this ADT on haskell. I haven't got luck
in so far. The problem is that referring to a `type family` constructed
from a term level function is not clear to me, even with singletons, as
I cannot guarantee such type family is defined. Currently I got this

    data Image (f :: Type -> Type) Type where
      Im :: Proxy (Sing t1 -> Sing (f t1)) -> f t1
         -> Image (Sing t1 -> Sing (f t1)) (f t1)

Which isn't exactly what the agda version is. Does anyone has an idea on
how to continue or has done this example before? I am perfectly OK with
being told it's not possible yet or what should I read.

-- 
-- Ruben
-- PGP: 4EE9 28F7 932E F4AD