Translating a pre-image witness from agda to haskell

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

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
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Translating a pre-image witness from agda to haskell

Li-yao Xia-2
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.
>
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.