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?
2 Likes
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!
2 Likes
awesome, let me play with it a bit!
1 Like
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
1 Like
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.
agreed that this could become as issue, but in my case I think Iāll never need the polymorphic version
1 Like
I see. My library is definitely overkill then.
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ā¦
1 Like
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.
1 Like
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.
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
.
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.
1 Like
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.
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.
1 Like
@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-type
s 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).