El 17/5/19 a las 11:56, ALeX Kazik escribió:

Hi Juan,

...

Now, the problem is what can I do to have a type that contains a single Int? Is there a sort of id for types so that I can write

Identity is the solution

f :: Example Identity Int -> Int f (Example i) = 2 * runIdentity i

Alex.

Thank you Alex, but this forces the use of runIdentity. I am aware that Identity Int and Int are isomorphic, but my problem is more aesthetic, I would like that the f t was t. I want to use it in a library and I don't want the users to be aware of details that should be irrelevant. Sometimes they will use lists, sometimes simple times, and would like that to be as transparent as possible. Juan Miguel -- Juan Miguel Vilar Torres Profesor titular de universidad Departamento de Lenguajes y Sistemas Informáticos Escuela Superior de Tecnología y Ciencias Experimentales Universitat Jaume I Av. de Vicent Sos Baynat s/n 12071 Castelló de la Plana (Spain) Tel: +34 964 72 8365 Fax: +34 964 72 8435 jvilar@uji.es

Juan Miguel Vilar writes:

El 17/5/19 a las 11:56, ALeX Kazik escribió:

...

...

Now, the problem is what can I do to have a type that contains a single Int? Is there a sort of id for types so that I can write

Identity is the solution

Thank you Alex, but this forces the use of runIdentity. [...] Sometimes they will use lists, sometimes simple times, and would like that to be as transparent as possible.

I do not like the sibling thread's suggestion of using closed type families, because I think the regulatity of always having the `f t` present is a nicer aesthetic. Using a type family to unwrap the `Identity` makes it noisier to write functions that consume your structure and are polymorphic in `f`. You can alleviate some of the syntactic noise of `runIdentity` with careful choices of type aliases or other helper functions. The type aliases (and `runFoo` functions) for monad transformers are good examples, and the `(==>)` function in dependent-sum[1] is a good additional example of the latter. To save you the click, DSum in dependent-sum is defined like this: data DSum tag f where !(tag a) :=> f a The (==>) helper is defined like this: (==>) :: Applicative f => tag a -> a -> DSum tag f tag ==> a = tag :=> f a So when f ~ Identity (or any other Applicative), the machinery becomes that much easier to use. -- Jack [1]: https://hackage.haskell.org/package/dependent-sum-0.5/docs/Data-Dependent-Su...

Juan Miguel Vilar writes:

El 17/5/19 a las 13:01, Jack Kelly escribió:

...

I do not like the sibling thread's suggestion of using closed type families...

I can't see the sibling thread you mentioned. On the other hand, as I said it is sort of an aesthetic question, so I think I can live with Identity.

Oh. In that case, here is the blog post they discussed, with the approach that I personally dislike: https://reasonablypolymorphic.com/blog/higher-kinded-data/ The key part is the HKD type family: {-# LANGUAGE TypeFamilies #-} -- "Higher-Kinded Data" type family HKD f a where HKD Identity a = a HKD f a = f a data Person' f = Person { pName :: HKD f String , pAge :: HKD f Int } deriving (Generic) HTH, -- Jack