Indexing into NP (SOP) https://www.reddit.com/r/haskell/comments/ik1yp1/monthly_hask_anything_september_2020/g4wx9m7/

IndexSOP.hs

{-# LANGUAGE
  ConstraintKinds,
  DataKinds,
  PolyKinds,
  GADTs,
  FlexibleInstances,
  MultiParamTypeClasses,
  ScopedTypeVariables,
  TypeFamilies,
  TypeApplications,
  TypeOperators,
  AllowAmbiguousTypes,
  UndecidableInstances #-}

import Data.Kind
import Data.Type.Bool
import Data.Type.Equality
import GHC.TypeNats

import Data.SOP

-- | The n-th element of list xs
type family At (n :: Nat) (xs :: [k]) :: k where
  At n xs = AtIf (0 == n) n xs

-- | Auxiliary definition for At
type family AtIf (eqz :: Bool) (n :: Nat) (xs :: [k]) :: k where
  AtIf 'True  n (x ': _) = x
  AtIf 'False n (_ ': xs) = At (n-1) xs

-- | Singleton type for Bool
data SBool (b :: Bool) where
  SFalse :: SBool 'False 
  STrue  :: SBool 'True

-- | Implicit singleton, or How to pattern-match on type-level booleans at run-time.
class IsBool b where
  bool :: SBool b

instance IsBool 'False where
  bool = SFalse

instance IsBool 'True where
  bool = STrue

-- | Conditional constraint.
type IfC b x y = (IsBool b, If b x y)
 
-- | The n-th element of a heterogeneous product.
class Index n xs f where
  index :: NP f xs -> f (At n xs)

instance (IfC (0 == n) (() :: Constraint) (Index (n - 1) xs f))  => Index n (x ': xs) f where
  index (x :* xs) =
    case bool @(0 == n) of
      STrue -> x
      SFalse -> index @(n-1) xs

example :: NP Maybe '[Int, Bool, String]
example = Just 0 :* Just True :* Just "False" :* Nil

main :: IO ()
main = do
  print (index @0 example)
  print (index @1 example)
  print (index @2 example)

IndexSOPFcf.hs

-- Same thing, but using first-class-families for some of the type-level boilerplate (IsBool, AtIf)

{-# LANGUAGE
  ConstraintKinds,
  DataKinds,
  PolyKinds,
  FlexibleInstances,
  MultiParamTypeClasses,
  ScopedTypeVariables,
  TypeFamilies,
  TypeApplications,
  TypeOperators,
  AllowAmbiguousTypes,
  UndecidableInstances #-}

import Data.Kind
import GHC.TypeNats

import Fcf hiding (type (-))

import Data.SOP

data At (n :: Nat) (xs :: [k]) :: Exp k
type instance Eval (At n xs) =
  Eval (If
    (Eval (TyEq 0 n))
    (UnMaybe (Error "Oops") Pure =<< Head xs)
    (UnMaybe (Error "Oops") (At (n - 1)) =<< Tail xs))
 
class Index n xs f where
  index :: NP f xs -> f (Eval (At n xs))

type IfC b x y = (IsBool b, If b x y)

instance (IfC (Eval (TyEq 0 n)) (() :: Constraint) (Index (n - 1) xs f))  => Index n (x ': xs) f where
  index (x :* xs) =
    _If @(Eval (TyEq 0 n))
      x
      (index @(n-1) xs)

example :: NP Maybe '[Int, Bool, String]
example = Just 0 :* Just True :* Just "False" :* Nil

main :: IO ()
main = do
  print (index @0 example)
  print (index @1 example)
  print (index @2 example)