Unboxed equality?

Learn
#1

I couldn’t find anything on Google. I want something like :~: that is unboxed, i.e. a ZeroBitType.

Does this exist?

#2

Not that I’m aware of, but you can more-or-less write it yourself:

{-# LANGUAGE
  MagicHash, UnliftedNewtypes, UnboxedTuples,
  GADTs, DataKinds, ExplicitNamespaces, RoleAnnotations
#-}

module ZeroBitEq (
  type (~#),
  refl#,
  withRefl#,
) where

-- base
import GHC.Exts (ZeroBitType)
import Unsafe.Coerce (unsafeCoerce)
import Data.Type.Equality ((:~:)(..))

type role (~#) nominal nominal
type (~#) :: k -> k -> ZeroBitType
newtype a ~# b = UnsafeRefl# (# #)

refl# :: (# #) -> a ~# a
refl# = UnsafeRefl#

withRefl# :: forall a b r. a ~# b -> (a ~ b => r) -> r
withRefl# !_ r = case unsafeCoerce Refl :: a :~: b of
  Refl -> r
3 Likes
#3

I do something similar in Bluefin, not for type equality but for a type level subset relation. It involves implementing the witness as

newtype In (a :: Effects) (b :: Effects) = In# (# #)

and then implementing some axioms, and some theorems on top of those axioms.

2 Likes
#4

Indeed; though I didn’t look too closely back then, I actually glimpsed this magic when I looked over bluefin previously.

Your have and inComp also roughly correspond to my withRefl#, but I notice that you only seem to be using inComp for transitivity? In a project I’m currently working on, I have similar proof tokens for scoping, where the Category instance provides reflexivity and transitivity:

data Scope

type role (~<) nominal nominal
type (~<) :: Scope -> Scope -> Type
data a ~< b = UnsafeSubScopeProof

instance Category (~<) where
  id      = UnsafeSubScopeProof
  !_ . !_ = UnsafeSubScopeProof

Like ~ and :>, it also has a constraint form <|:

reflect :: p ~< q -> (p <| q => r) -> r

But here’s the clever part—GHC can actually infer reflexivity and transitivity if you phrase the class just right! Ultimately, I don’t actually need the value level proof tokens, they just give you better error messages in prototyping.

type (<|) = SubScope

class SubScopeEndo (s :: Scope)

class    (SubScopeEndo p => SubScopeEndo q) => SubScope p q where
  auto :: p ~< q
instance (SubScopeEndo p => SubScopeEndo q) => SubScope p q where
  auto = UnsafeSubScopeProof

Credit to the authors of The Foil for this technique.

1 Like
Trials & Tribulations for Transitivity
#5

Thanks! I already do this but it seems like something that you’d expect to be in base.

#6

Ultimately we’d want :~: to be unboxed itself (or perhaps more precisely, unlifted, zero-width). I’m not actually sure why it’s not. I guess part of the reason is that ~ is a lifted constraint. I don’t understand that either. Type equality doesn’t require any non-trivial information. Couldn’t it be an unlifted, zero-width constraint?

1 Like
#7

afaiu it is. i.e. the ~ in real GADTs (not the ones made with lifted equality and -XExistentialTypes) compile to an unlifted equality (~#). However, there’s no syntax for unlifted equality, because iirc it doesn’t have the right kind to even fit into the surface level syntax or something like this. You can, however, make GHC reveal what it’s really doing, by asking it what (~~) is. In order to do so, open a GHCi, then import GHC.Types, set -fprint-equality-relations and type :i (~~).

You can also see it if you define a

module Eq  where 
import Prelude ()
data Eq a b where 
  Refl :: Eq a a

and then look at the core of the Refl constructor.

2 Likes