Hi Ruben, A general way to represent functions in types in Haskell is via defunctionalization. - https://typesandkinds.wordpress.com/2013/04/01/defunctionalization-for-the-w... - http://h2.jaguarpaw.co.uk/posts/hkd-pattern-type-level-ski/ - https://blog.poisson.chat/posts/2018-08-06-one-type-family.html "Defunctionalization" essentially gives you -- A kind for function symbols type a :-> b = ... -- A way to apply function symbols type family (f :: a :-> b) @@ (x :: a) :: b Equipped with that here's how you could define Image data Image (f :: a :-> b) :: b -> Type where Im :: Sing x -> Image f (f @@ x) There's a few variants depending on where you want to put singletons, but I think a good rule of thumb if you come from Agda is to not include type parameters and indices (f and y), only terms actually introduced by the constructor (x). Defunctionalization in general has a great many applications. There's this great Compose 2019 talk about it: - http://www.pathsensitive.com/2019/07/the-best-refactoring-youve-never-heard.... Li-yao On 7/22/19 1:20 AM, Ruben Astudillo wrote:

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.