linear_horrors.hs

{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FunctionalDependencies #-}

import Data.Kind (Type, Constraint)

-- an unconstrained dynamic type is "inaccessible", and we'll use it to throw away values we don't need
data Bin where
    Inaccessible :: a %1 -> Bin

-- we only ever need one, though
(<?>) :: Bin %1 -> Bin %1 -> Bin
(Inaccessible l) <?> (Inaccessible r) = Inaccessible (l, r)

-- a function that produces `b`, and may "throw away" values
newtype AffFn a b = AffFn (a %1 -> (b, Bin))
type (-?>) = AffFn

($?) :: (a -?> b) %1 -> a %1 -> (b, Bin)
(AffFn f) $? x = f x

-- in the world of -?>, anything can be destroyed, though duplication is still not allowed
destroy :: a -?> ()
destroy = AffFn (\x -> ((), Inaccessible x))

-- ofc we have composition
affComp :: (a -?> b) %1 -> (b -?> c) %1 -> (a -?> c)
affComp (AffFn f) (AffFn g) = AffFn (\x -> case f x of (x2, bin) -> case g x2 of (x3, bin2) -> (x3, bin <?> bin2))

-- i would love to use an associated type, but then i can't...
class Choose l r h | h -> l, h -> r where
    left :: h -?> l
    right :: h -?> r

instance Choose a b (a, b) where
    left :: (a, b) -?> a
    left = AffFn (\(a, b) -> (a, Inaccessible b))

    right :: (a, b) -?> b
    right = AffFn (\(a, b) -> (b, Inaccessible a))

-- ...use an existential type to represent an eliminator-only type
data Dyn (c :: Type -> Constraint) where
    Erased :: c a => a %1 -> Dyn c

-- so given an `a & b`, you must make the choice between using `left` or `right`, never both
type a & b = Dyn (Choose a b)

-- and then we need this for DUMB and STUPID reasons
instance Choose a b (a & b) where
    left = AffFn (\(Erased h) -> left $? h)
    right = AffFn (\(Erased h) -> right $? h)

pack :: (a, b) %1 -> a & b
pack = Erased

-- but if we have an ! in the mix...
data Ur a where
    Ur :: a -> Ur a -- no %1

-- we can convert out!
unpack :: Ur (a & b) %1 -> (Ur a, Ur b)
unpack (Ur choice) =
    let (lft, _) = left $? choice
        (rgt, _) = right $? choice in
    (Ur lft, Ur rgt)