Type instances - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Asad Saeeduddin

Can type instances be overlappable?

Lysxia

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-

Asad Saeeduddin

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.

Asad Saeeduddin

with open type families I mean

Lysxia

There's no way to argue with the compiler about this

Asad Saeeduddin

I'm trying to do something like this:

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
Asad Saeeduddin

i tried the Fcf approach as well, but I run into the same issue with that catch all case at the end

Asad Saeeduddin

maybe I need a closed type family here

Lysxia

Yeah that doesn't work with open families.

Asad Saeeduddin

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

Asad Saeeduddin

like, this works:

data EProd :: [*] -> Exp *

type instance Eval (EProd '[]) = ()
type instance Eval (EProd (x ': xs)) = (x, Eval (EProd xs))

data ESum :: [[*]] -> Exp *

type instance Eval (ESum '[]) = Void
type instance Eval (ESum (x ': xs)) = Either (Eval (EProd x)) (Eval (ESum xs))

type family Normalized x
  where
  Normalized (Either x Void) = Normalized x
  Normalized (Either Void x) = Normalized x
  Normalized (Either x y) = Either (Normalized x) (Normalized y)

  Normalized ((), x) = Normalized x
  Normalized (x, ()) = Normalized x
  Normalized (x, y) = (Normalized x, Normalized y)

  Normalized x = x
Lysxia

yeah that's a common problem with closed type families

Asad Saeeduddin

but idk if there's any hope of me being able to teach it how to thread the term level stuff through

Asad Saeeduddin

do you think Case from Fcf can help me do this?

Asad Saeeduddin

I couldn't figure out how to deal with the type parameters of Either or (,) when using it

Lysxia

That's why I prefer to use boolean equality tests instead of plain closed type families.

Lysxia

You'll have the same problem with Case... I should probably fix that.

Asad Saeeduddin

Where do you get the boolean to test in the first place?

Lysxia

Use Data.Type.Equality.==

type family Normalized x where
  Normalized (Either x y) = If (x == Void) (Normalized y) (If (y == Void) (Normalized x) (Either (Normalized x) (Normalized y)))
  Normalized (x, y) = ...
Lysxia

I'm not sure what to do about the catchall though...

Asad Saeeduddin

so the output of that is Exp *, right?

Lysxia

The snippet above does not use fcfs but you might want to use fcfs, I'm not sure.

Lysxia

Oh I forgot some nested calls to Normalized. This blows up exponentially if you don't use something like fcfs.

Lysxia

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?

Asad Saeeduddin

what I want ultimately is for :kind! Magic [a] to give me () + (a, [a])

Asad Saeeduddin

it's fine for the stuff inside the fields to be a pair, I don't look past the structure of the outermost datatype

Asad Saeeduddin

I'm basically operating on the two level list thing SOP gives you

Asad Saeeduddin

it's easy to get to a point where you get something like () + (a * [a] * ()) + Void

Asad Saeeduddin

I just want to get rid of those useless () and Void markers

Asad Saeeduddin

with fcf I can write this:

data EProd :: [*] -> Exp *

type instance Eval (EProd '[]) = ()
type instance Eval (EProd (x ': xs)) = (x, Eval (EProd xs))

data ESum :: [[*]] -> Exp *

type instance Eval (ESum '[]) = Void
type instance Eval (ESum (x ': xs)) = Either (Eval (EProd x)) (Eval (ESum xs))

and it's annoying but I can do the evidence threading for that, and the result is that I can do:

λ> :kind! Eval (ESum '[ '[], '[Int] ])
Eval (ESum '[ '[], '[Int] ]) :: *
= Either () (Either (Int, ()) Void)
Lysxia

Asad Saeeduddin said:

it's fine for the stuff inside the fields to be a pair, I don't look past the structure of the outermost datatype

How can that work? If you have a = () * (), then Normalize (() + ((() * ()) * [() * ()] * ()) will just destroy everything.

Asad Saeeduddin

when I say "I don't look past the structure of the outermost datatype", I mean I don't look at the (,) in data MyFoo = Foo (x, y) | Bar Int

Lysxia

The definition of Normalize you gave seems like it's looking at it.

Asad Saeeduddin

i'm starting out from a representation like '[ '[(x, y)], '[Int] ]. I fold the inner lists with (,) and (), and the outer list with Either and Void

Asad Saeeduddin

hmm. idk exactly, maybe it is

Lysxia

And I disagree those markers are useless, they make the structure regular so you don't have to deal with weird corner cases

Asad Saeeduddin

by my lights what I'd end up with is ((x, y), ()) + (Int, ()) + Void

Lysxia

As evidenced by the trouble you're going through trying to get rid of them.

Asad Saeeduddin

The markers make it too awkward to use this representation for anything useful

Asad Saeeduddin

what I want Magic (((x, y), ()) + (Int, ()) + Void) to give me is (x, y) + Int

Asad Saeeduddin

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

Asad Saeeduddin

I think what I probably want is this:

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
Asad Saeeduddin

that gives:

λ> :kind! ENormalize (Eval (ESum '[ '[(String, Char)], '[Int] ]))
ENormalize (Eval (ESum '[ '[(String, Char)], '[Int] ])) :: *
= Either (String, Char) Int
Asad Saeeduddin

I wonder the corresponding term level recursion can be handled using something like @TheMatten's FCI library

Asad Saeeduddin

in the sense that I can have literal products and coproducts of instances

Asad Saeeduddin

if I can somehow reflect type level equality tests to the term level, I can use that to choose between instances

Asad Saeeduddin

@Lysxia Do you think I can use Data.Type.Equality to automatically fill in the boolean in here and resolve the ambiguity:

class 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)

class ENormalize (b :: Bool) (e :: *) (n :: *)
  where
  enormalize :: Proxy b -> Iso' e n

instance
  TNormalize b x x' =>
  ENormalize 'False (x + Void) x'
  where
  enormalize _ = iso (either (fwd (tnormalize $ Proxy @b)) absurd) (Left . bwd (tnormalize $ Proxy @b))

instance
  (TNormalize a x x', ENormalize b y y') =>
  ENormalize 'True (x + y) (x' + y')
  where
  enormalize _ = iso
    (bimap (fwd $ tnormalize $ Proxy @a) (fwd $ enormalize $ Proxy @b))
    (bimap (bwd $ tnormalize $ Proxy @a) (bwd $ enormalize $ Proxy @b))
Asad Saeeduddin

Right now this only works with AllowAmbiguousTypes turned on

Lysxia
class (IsRightUnit p ~ b) => TNormalize b p n
  where ...
Asad Saeeduddin

then the problem moves to how to instantiate IsRightUnit, no?

Asad Saeeduddin

or is that a non-issue?

Asad Saeeduddin

I tried this:

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')’
Lysxia

Yes you need to add it to your instance constraints

Asad Saeeduddin

ah yes, I was being stupid

Asad Saeeduddin

great. so do you know how to actually view what a functional dependency determines a parameter to be?

Lysxia

other than hacks to just get type inference to run...

Lysxia
evalFunDep :: forall x y. ClassWithFunDep x y => Proxy y
evalFunDep = Proxy

test = evalFunDep @MyX

-- In ghci:
-- :t test