Instances for type families

[marcosh]

I have a type family like

type family CountryCodeContext (countryCodePresence :: CountryCodePresence) t where
  CountryCodeContext 'WithCountryCode t = t
  CountryCodeContext 'MaybeCountryCode t = Maybe t
  CountryCodeContext 'NoCountryCode t = ()

where

data CountryCodePresence
  = WithCountryCode
  | MaybeCountryCode
  | NoCountryCode

Is it possible to convince the compiler somehow that Show t => CountryCodeContext countryCodePresence t? If I try to write it directly I get a Illegal type synonym family application ‘CountryCodeContext countryCodePresence t’ error message.

Alternatively, is there a standard way to rewrite this code so that defining instances is possible?

[tomjaguarpaw]

Aha! As it happens I have just written a library for making this kind of thing simpler. It’s very much in draft form, but certainly usable for what you’re doing. I suggest you start by reading the example, including where the instances are defined.

I’m happy to chat more about this. Just let me know!

[marcosh]

awesome, let me play with it a bit!

[marcosh]

I tried to use the library, but in the end it was bringing in more complexity than what I needed.

Since the type I’m really interested in is

data Phone (hasCountryCode :: CountryCodePresence) = Phone
  { number :: Number
  , countryCode :: CountryCodeContext hasCountryCode CountryCode
  }

I can just use

deriving stock instance Show (Phone 'WithCountryCode)
deriving stock instance Show (Phone 'MaybeCountryCode)
deriving stock instance Show (Phone 'NoCountryCode)

That should be enough for my needs at the moment

[tomjaguarpaw]

The problem with that will come when you want to use show in a function of type Phone t -> Something. For example, try to write the following. What type class constraint can you put on t?

myShow :: ??? => Phone hasCountryCode -> String
myShow p = "The Phone is: " ++ show p

EDIT: Actually, I take that back. Show (Phone hasCountryCode) works fine in this case. I guess it’s only in more complex cases where it becomes difficult.

[marcosh]

agreed that this could become as issue, but in my case I think I’ll never need the polymorphic version

[tomjaguarpaw]

I see. My library is definitely overkill then.

[michaelpj]

I think I have been trying to do something similar recently. I have a WIP branch redoing some stuff inside lsp, and it has exactly this problem: we have a kind k that classifies the “methods” for a JSON-RPC server, and then we have a bunch of type families that pick out the various types for e.g. the message params. I then get exactly these sorts of problems when I want, say, a ToJSON (MessageParams (m :: k)) constraint.

I came up with this: https://github.com/haskell/lsp/blob/mpj/typed-json-rpc/lsp/jsonrpc-typed/JSONRPC/Types/Method.hs#L18

I think it’s quite similar to your Index typeclass. Some differences:

• Use singletons for the singletons, so I use Sing instead of Constructor; and similarly constructorToValue is just something from singletons
• Use GEq @k Sing instead of your eqT

I think it’s nice to use the singletons tools, it makes things a little more standard. I need to look at your trick with Dict to see what the difference is there, but it looks like you might have ended up with better ergonomics than me. I end up having to define lots of ad-hoc typeclasses in order to get something that can be used unsaturated, which is quite unsatisfying…

[michaelpj]

A few further observations:

• Matchable is pretty much SingI from singletons
• I think your use of toType could be replaced by SingKind.toSing

The use of a wrapper type to be able to derive instances is nice. I tried that and went back to just trying to get instances for the type family applications themselves. But it does end up being a bit clumsy.

[tomjaguarpaw]

Yeah, much of what I’m doing is well explored. If you check the commits from yesterday you’ll see I renamed Singleton to Constructor I never managed to understand singletons but much of the knowledge it contains is floating around in the ether, so I decided to write a library that was less baffling, but most importantly, allows nice deriving of instances.

If by GEq you mean Data.GADT.Compare then I find that pretty unergonomic because you really don’t want to to have to wrap your SingI constraints into a type to apply geq.

I should probably dive into singletons again and try to find the exact correspondence, but I know that a lot of it is about promoting value level functions to the type level, which is not something I’m particularly interested in.

[tomjaguarpaw]

I think I have been trying to do something similar recently.

Oh wow, this is really astonishingly similar for something we were both working on a couple of days ago Your bring is basically my withMatchable.

[michaelpj]

FWIW, I resisted using singletons for ages, but I really don’t regret it (I learned it from this truly exceptional blog post series: Introduction to Singletons (Part 1) · in Code). It has a lot of the tools that I want, and it’s nice and consistent with existing terminology and works with other libraries.

It’s also the case that the rest of the code I’m writing needs singletons pervasively, so it all fits together nicely. I guess if you haven’t found yourself needing them when you use your types, then it’s not so compelling.

[tomjaguarpaw]

Well, I know I need singletons the concept but I don’t know if I need singletons the library. What are you using singletons the library for, other than the code you just linked?

EDIT: Oh, do you mean you use the library to generate the singletons?

EDIT2: I see I’ve reinvented some other stuff from singletons, such as KindOf as TypeOf. The main complaint I have against the library is that it’s not written in a way that gives you any clue about how to use it or even what you might use it for.

[michaelpj]

No, I mostly don’t use singletons-th to generate singletons (although you can do, and I do this in some tests). I just need singletons for “normal dependently-typed-programming in Haskell” reasons, e.g. I have a type for a JSON-RPC message that has a method singleton so you can look at it to get information about the method to the type level. I also need singletons for things that I’m not directly using as dataype indices.

Do I need singletons-the-library for that? I guess not (the existing lsp implementation has “singletons” but doesn’t use singletons), but I do think it’s somewhat more standard in the ecosystem, which increases the chance that someone will understand the implementation. I also find it reassuring if something is in singletons: I’m very much feeling my way around here, so if I want something and it’s in singletons I feel reassured that it’s probably not a crazy thing to want e.g. SingKind

The main complaint I have against the library is that it’s not written in a way that gives you any clue about how to use it or even what you might use it for.

I cannot recommend the blog post series I linked to highly enough, it’s really very good.

[tomjaguarpaw]

@michaelpj

I cannot recommend the blog post series I linked to highly enough, it’s really very good.

@michaelpj Thanks for the recommendation of this interesting blog series! I’ve read all four parts. How many of the parts cover what you use in lsp? Or do you use stuff even beyond what is covered in that blog series?

indexed-types can handle everything that’s covered in parts 1 and 2. I haven’t needed anything from parts 3 or 4 yet (which are mostly type level functions).