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

[Li-yao Xia]

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-win/
- 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.html

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.
>