Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
{-# language FlexibleInstances, DataKinds, TypeFamilies, TypeOperators, MultiParamTypeClasses, UndecidableInstances, UndecidableSuperClasses, FunctionalDependencies, PolyKinds #-}
import GHC.Exts
import GHC.TypeLits
import Data.Proxy
type family AllC (c :: k -> Constraint) (xs :: [k]) :: Constraint where
AllC _ '[] = ()
AllC c (k ': ks) = (c k, AllC c ks)
class (KnownNat res, AllC KnownNat ns) => Product (ns :: [Nat]) (res :: Nat) | ns -> res
instance {-# Overlapping #-} KnownNat n => Product '[n] n
instance
( KnownNat res
, KnownNat n
, KnownNat answer
, answer ~ (n * res)
, Product ns res
, AllC KnownNat ns
) => Product (n ': ns) answer
-- *Main Data.Proxy> :t mult (Proxy :: Proxy '[1,3,3])
-- mult (Proxy :: Proxy '[1,3,3]) :: Proxy 9
mult :: Product ns m => Proxy ns -> Proxy m
mult _ = Proxy
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.