[Haskell-cafe] Using a non fully saturated type family

[Oleg Grenrus]

You cannot without a hacks until
https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0242-unsaturated-type-families.rst
is implemented.

One hack is to use defunctionalisation, as in singletons library. Check 
their definition for Sigma
https://hackage.haskell.org/package/singletons-3.0/docs/Data-Singletons-Sigma.html
where (@@) is a synonym for Apply type family, and your Tag is
essentially Sing for Bool.

- Oleg

On 9.9.2021 18.35, Ruben Astudillo wrote:
> Hello Cafe.
>
> I am trying to encode a version of sigma types using GADTs for the tag and a
> type family as the function between the GADT and the universe of types. My
> code looks like this (notice the use of StandaloneKindSignatures).
>
>     --- | dependent.hs
>     {-# language RankNTypes, PolyKinds, TypeFamilies, GADTs #-}
>     {-# language StandaloneKindSignatures, DataKinds #-}
>     module Main where
>
>     import Data.Kind (Type)
>     import Data.Functor.Identity
>
>     main :: IO ()
>     main = return ()
>
>     type Tag :: Bool -> Type
>     data Tag b where
>       STrue :: Tag True
>       SFalse :: Tag False
>
>     type ApplyTag :: Bool -> Type
>     type family ApplyTag t where
>       ApplyTag 'True = Int
>       ApplyTag 'False = Char
>
>     type Sigma :: forall k. (k -> Type) -> (k -> Type) -> Type
>     data Sigma t f where
>       (:&:) :: forall t f a. t a -> f a -> Sigma t f
>
>     ex :: Sigma Tag ApplyTag
>     ex = STrue :&: 27
>
> The error I get is
>
>     dependent.hs:24:7: error:
>         • The type family ‘ApplyTag’ should have 1 argument, but has been
>           given none
>         • In the type signature: ex :: Sigma Tag ApplyTag
>        |
>     24 | ex :: Sigma Tag ApplyTag
>        |       ^^^^^^^^^^^^^^^^^^
>
> which is true! How can I recover the intuition of type families being
> functions at the type level?
>