An attempt to understand Haskell's various ways to get a partially-collapsed type hierarchy and partially-dependent types, via algebraic structures implemented as typeclasses.

Field.hs

{-# LANGUAGE EmptyDataDecls, TypeOperators, LiberalTypeSynonyms, ExistentialQuantification, ExplicitForAll #-}
{-# LANGUAGE GADTSyntax, GADTs, DuplicateRecordFields, NamedFieldPuns, MultiParamTypeClasses, FlexibleContexts, TypeSynonymInstances, FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies, TypeFamilies, TypeFamilyDependencies, ConstraintKinds, ScopedTypeVariables #-}
{-# LANGUAGE DataKinds, PolyKinds, KindSignatures, TypeInType, TypeApplications, ImplicitParams, NamedWildCards, RankNTypes #-}
{-# LANGUAGE ExplicitNamespaces, MonoLocalBinds, DisambiguateRecordFields, ConstrainedClassMethods #-}
--- ^ I just grabbed anything that looked remotely useful.

module Algebraics.Data.Field where

import GHC.TypeLits
import GHC.TypeNats
import Data.Kind hiding ((*))
import Data.Type.Equality

class (Eq k) => MagmaId k where
  type family Zero :: k
  -- data Add  :: k -> k -> k
  -- addIdl :: forall (x :: k) . (Add x Zero :~: x)
  -- addIdR :: forall (x :: k) . (Add Zero x :~: x)

-- Doesn't work; `GHC.Types.Nat` isn't part of `Eq`, since it isn't actually the Peano numbers. No inductive pattern matching is possible, apparently.
instance MagmaId Nat where
  type instance Zero = 0
  -- data Add  = '(+)
  -- addIdl = Refl
  -- addIdR = Refl