class Normalize (e :: *)
where
type Normalized (e :: *) :: *
instance Normalize (Either x Void)
where
type Normalized (Either x Void) = Normalized x
instance Normalize (Either Void x)
where
type Normalized (Either Void x) = Normalized x
instance Normalize (x, ())
where
type Normalized (x, ()) = Normalized x
instance Normalize ((), x)
where
type Normalized ((), x) = Normalized x
instance Normalize x
where
type Normalized x = x
so that the user, who will more naturally arrive at a (x, y) + Int than a ((x, y), ()) + (Int, ()) + Void, will be able to convert their stuff to a data MyFoo = Foo (x, y) | Bar Int
type family TNormalize x
where
TNormalize (x, ()) = x
TNormalize (x, y) = (x, TNormalize y)
TNormalize x = x
type family ENormalize x
where
ENormalize (Either x Void) = TNormalize x
ENormalize (Either x y) = Either (TNormalize x) (ENormalize y)
ENormalize x = TNormalize x
type family IsRightUnit p :: Bool
where
IsRightUnit (x, ()) = 'True
IsRightUnit (x, y) = 'False
class
(IsRightUnit p ~ b) =>
TNormalize (b :: Bool) (p :: *) (n :: *)
where
tnormalize :: Proxy b -> Iso' p n
instance TNormalize 'True (x, ()) x
where
tnormalize _ = iso fst (, ())
instance
TNormalize b y y' =>
TNormalize 'False (x, y) (x, y')
where
tnormalize _ = iso (second $ fwd $ tnormalize $ Proxy @b) (second $ bwd $ tnormalize $ Proxy @b)
but it doesn't like the last instance anymore:
[typecheck] [E] /mnt/data/depot/git/haskell/experiments/co-optics/src/SOP/Sums2.hs:80:3: error:
• Could not deduce: IsRightUnit (x, y) ~ 'False
arising from the superclasses of an instance declaration
from the context: TNormalize b y y'
bound by the instance declaration
at /mnt/data/depot/git/haskell/experiments/co-optics/src/SOP/Sums2.hs:(80,3)-(81,34)
• In the instance declaration for
‘TNormalize 'False (x, y) (x, y')’
Can type instances be overlappable?
You can have overlap in a closed type family, or in an open type family as long as the compiler can see they're confluent. For example:
https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Type-Bool.html#t:-38--38-
Is confluence something I can mark explicitly, or if the compiler isn't happy with my definition does that just mean I can't do it.
with open type families I mean
There's no way to argue with the compiler about this
I'm trying to do something like this:
i tried the Fcf approach as well, but I run into the same issue with that catch all case at the end
maybe I need a closed type family here
Yeah that doesn't work with open families.
the problem is if I do it as a closed type family and it's not injective it becomes very difficult to thread the term level evidence through
like, this works:
yeah that's a common problem with closed type families
but idk if there's any hope of me being able to teach it how to thread the term level stuff through
do you think
Case
fromFcf
can help me do this?I couldn't figure out how to deal with the type parameters of
Either
or(,)
when using itThat's why I prefer to use boolean equality tests instead of plain closed type families.
You'll have the same problem with
Case
... I should probably fix that.Where do you get the boolean to test in the first place?
Use
Data.Type.Equality.==
I'm not sure what to do about the catchall though...
so the output of that is
Exp *
, right?The snippet above does not use fcfs but you might want to use fcfs, I'm not sure.
Oh I forgot some nested calls to
Normalized
. This blows up exponentially if you don't use something like fcfs.Do you even need overlap though? What if one of the fields is a pair? Why not mark fields with an
Identity
or something similar?what I want ultimately is for
:kind! Magic [a]
to give me() + (a, [a])
it's fine for the stuff inside the fields to be a pair, I don't look past the structure of the outermost datatype
I'm basically operating on the two level list thing SOP gives you
it's easy to get to a point where you get something like
() + (a * [a] * ()) + Void
I just want to get rid of those useless
()
andVoid
markerswith fcf I can write this:
and it's annoying but I can do the evidence threading for that, and the result is that I can do:
Asad Saeeduddin said:
How can that work? If you have
a = () * ()
, thenNormalize (() + ((() * ()) * [() * ()] * ())
will just destroy everything.when I say "I don't look past the structure of the outermost datatype", I mean I don't look at the
(,)
indata MyFoo = Foo (x, y) | Bar Int
The definition of
Normalize
you gave seems like it's looking at it.i'm starting out from a representation like
'[ '[(x, y)], '[Int] ]
. I fold the inner lists with(,)
and()
, and the outer list withEither
andVoid
hmm. idk exactly, maybe it is
And I disagree those markers are useless, they make the structure regular so you don't have to deal with weird corner cases
by my lights what I'd end up with is
((x, y), ()) + (Int, ()) + Void
As evidenced by the trouble you're going through trying to get rid of them.
The markers make it too awkward to use this representation for anything useful
what I want
Magic (((x, y), ()) + (Int, ()) + Void)
to give me is(x, y) + Int
so that the user, who will more naturally arrive at a
(x, y) + Int
than a((x, y), ()) + (Int, ()) + Void
, will be able to convert their stuff to adata MyFoo = Foo (x, y) | Bar Int
and vice versa
I think what I probably want is this:
that gives:
I wonder the corresponding term level recursion can be handled using something like @TheMatten's FCI library
in the sense that I can have literal products and coproducts of instances
if I can somehow reflect type level equality tests to the term level, I can use that to choose between instances
@Lysxia Do you think I can use
Data.Type.Equality
to automatically fill in the boolean in here and resolve the ambiguity:Right now this only works with
AllowAmbiguousTypes
turned onthen the problem moves to how to instantiate
IsRightUnit
, no?or is that a non-issue?
I tried this:
but it doesn't like the last instance anymore:
Yes you need to add it to your instance constraints
ah yes, I was being stupid
great. so do you know how to actually view what a functional dependency determines a parameter to be?
the way
:kind!
doesNo idea
other than hacks to just get type inference to run...