Is it possible to use a type family as a higher-order "type function" to pass to another type family? A simple example would be the following code:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where
import GHC.TypeLits as T
type family Apply (f :: Nat -> Nat -> Nat) (n :: Nat) (m :: Nat) :: Nat where
Apply f n m = f n m
type family Plus (n :: Nat) (m :: Nat) :: Nat where
Plus n m = n T.+ m
type family Plus' (n :: Nat) (m :: Nat) :: Nat where
Plus' n m = Apply (T.+) n m
The first declaration of Plus
is valid, while the second one (Plus'
) produces the following error:
Test.hs:19:3: error:
• The type family ‘+’ should have 2 arguments, but has been given none
• In the equations for closed type family ‘Plus'’
In the type family declaration for ‘Plus'’
|
19 | Plus' n m = Apply (T.+) n m
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Is there a way to use the Apply
type function to implement Plus
?
EDIT A commenter linked to the feature request report at https://ghc.haskell.org/trac/ghc/ticket/9898. It mentions the singleton
library. I would be happy with an example of using it or other "workarounds" to achieve a similiar effect of abstracting over the arithmetic operations on Nat
such as +
, *
, -
and Mod
.
(T.+)
as an argument because it is defined as a type family. This wouldn't be a problem though for e.g. a plain parametric data type. – leftaroundaboutsingletons
, another way of doing defunctionalization isfirst-class-families
, see blog.poisson.chat/posts/2018-08-06-one-type-family.html (I'm the author). – Li-yao Xia