these-n-labeled.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module W where

import Data.Kind
import Data.Proxy
import GHC.OverloadedLabels
import GHC.TypeLits

data Labeled name ty = name ::: ty

data These :: [Labeled Symbol Type] -> Type where
  This :: a -> These ((name ::: a) : xs)
  That :: These xs -> These (a : xs)
  These :: a -> These xs -> These (name ::: a : xs)

class ShowTheseElems xs where
  showTheseElems :: These xs -> [(String, String)]

showLabeled :: forall name ty. (KnownSymbol name, Show ty) => ty -> (String, String)
showLabeled x = (symbolVal (Proxy @name), show x)

instance (KnownSymbol name, Show ty) => ShowTheseElems '[name ::: ty] where
  showTheseElems (This x) = [showLabeled @name x]
  showTheseElems That {} = error "impossible case for singleton These: That"
  showTheseElems These {} = error "impossible case for singleton These: These"

instance (KnownSymbol name, Show ty, ShowTheseElems (x : xs)) => ShowTheseElems (name ::: ty : (x : xs)) where
  showTheseElems (This x) = [showLabeled @name x]
  showTheseElems (That xs) = showTheseElems xs
  showTheseElems (These x xs) = showLabeled @name x : showTheseElems xs

instance ShowTheseElems xs => Show (These xs) where
  show t =
    case showTheseElems t of
      [nv] -> showSingle nv
      nvs -> "these [" <> commas (map showSingle nvs) <> "]"
    where
      commas = foldr1 (\a b -> a <> ", " <> b)
      showSingle (name, val) = "#" <> name <> " " <> val

class TheseSingle name (xs :: [Labeled Symbol Type]) ty | name xs -> ty where
  has :: These xs -> Maybe ty
  only :: ty -> These xs

instance {-# OVERLAPS #-} TheseSingle name (name ::: ty : xs) ty where
  has (This x) = Just x
  has (That _) = Nothing
  has (These x _) = Just x
  only x = This x

instance TheseSingle name xs ty => TheseSingle name (x : xs) ty where
  has (This _) = Nothing
  has (That xs) = has @name xs
  has (These _ xs) = has @name xs
  only x = That (only @name x)

instance TheseSingle name xs ty => IsLabel name (ty -> These xs) where
  fromLabel = only @name

instance TheseSingle name xs ty => IsLabel name (These xs -> Maybe ty) where
  fromLabel = has @name

mergeByFirst :: These xs -> These xs -> These xs
mergeByFirst (This a) (This _) = This a
mergeByFirst (This a) (That b) = These a b
mergeByFirst (This a) (These _ b) = These a b
mergeByFirst (That b) (That b') = That (mergeByFirst b b')
mergeByFirst (That b) (These a b') = These a (mergeByFirst b b')
mergeByFirst (These a b) (These _ b') = These a (mergeByFirst b b')
mergeByFirst b a = mergeByFirst a b

these :: [These xs] -> These xs
these = foldr1 mergeByFirst

type User = These ["name" ::: String, "age" ::: Int, "admin" ::: Bool]

users :: [User]
users =
  [ #name "kana",
    #age 23,
    #admin True,
    these [#name "kana", #age 23],
    these [#name "kana", #admin True],
    these [#admin True, #age 23],
    these [only @"name" "kana", only @"age" 23, only @"admin" True]
  ]

someUserField :: User -> String
someUserField (#name -> Just _) = "has name"
someUserField (#age -> Just _) = "has age"
someUserField (#admin -> Just _) = "has admin"
someUserField _ = undefined

main :: IO ()
main = do
  traverse print users
  putStrLn (someUserField (#age 42))