Scratch.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}

module Scratch () where

import Data.Kind (Constraint, Type)
import Numeric.Natural (Natural)

newtype InputA = InputA Word deriving newtype (Show)
newtype InputB = InputB Int deriving newtype (Show)
newtype OutputA = OutputA Natural
  deriving stock Show
  deriving newtype (Read)
newtype OutputB = OutputB Integer
  deriving stock Show
  deriving newtype (Read)

{-
type family OutputType t where
  OutputType InputA = OutputA
  OutputType InputB = OutputB

f :: inp -> OutputType inp
f t = read $ show t

^ does not type check, because GHC does not understand the the type family is partial
 -}

-- Using associated type families, on a class targeting the input

class (Show input, Read (ToOutputType input)) => ToOutput input where
  type ToOutputType input :: Type

instance ToOutput InputA where
  type ToOutputType InputA = OutputA

instance ToOutput InputB where
  type ToOutputType InputB = OutputB

f :: ToOutput inp => inp -> ToOutputType inp
f i = read $ show i

x :: OutputA
x = f (InputA 42)

-- Using associated data families, on a class targeting a "ProtocolStep"

data ProtocolStep = StepA | StepB

type ProtocolPair :: ProtocolStep -> Constraint
class (Show (ProtocolInput step), Read (ProtocolOutput step)) => ProtocolPair step where
  data family ProtocolInput step :: Type
  data family ProtocolOutput step :: Type

instance ProtocolPair 'StepA where
  newtype ProtocolInput 'StepA = ProtocolInputA Word deriving newtype (Show)
  newtype ProtocolOutput 'StepA = ProtocolOutputA Natural
    deriving stock (Show)
    deriving newtype (Read)

instance ProtocolPair 'StepB where
  newtype ProtocolInput 'StepB = ProtocolInputB Int deriving newtype (Show)
  newtype ProtocolOutput 'StepB = ProtocolOutputB Integer
    deriving stock (Show)
    deriving newtype (Read)

g :: ProtocolPair step => ProtocolInput step -> ProtocolOutput step
g i = read $ show i

y :: ProtocolOutput 'StepA
y = g (ProtocolInputA 42)

-- >>> y
-- ProtocolOutputA 42

-- Using associated type families, on a class targeting a "ProtocolStep"
-- We need TypeFamilyDependencies a.k.a Injective Type Families so that GHC can deduce
-- what is the step when given the input type, to avoid ambiguity

type ProtocolPair2 :: ProtocolStep -> Constraint
class (Show (ProtocolInput2 step), Read (ProtocolOutput2 step)) => ProtocolPair2 step where
  type family ProtocolInput2 step = inp | inp -> step
  type family ProtocolOutput2 step = out | out -> step

instance ProtocolPair2 'StepA where
  type ProtocolInput2 'StepA = InputA
  type ProtocolOutput2 'StepA = OutputA

instance ProtocolPair2 'StepB where
  type ProtocolInput2 'StepB = InputB
  type ProtocolOutput2 'StepB = OutputB

h :: forall step. ProtocolPair2 step => ProtocolInput2 step -> ProtocolOutput2 step
h i = read @(ProtocolOutput2 step) $ show @(ProtocolInput2 step) i

z :: OutputA
z = h (InputA 42)