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

[Li-yao Xia]

Hi Ruben,

Oleg mentioned defunctionalization as one solution. Another is to wrap 
the type family in a newtype.

     newtype ApplyTagT t = ApplyTagT (ApplyTag t)

Sigma Tag ApplyTagT is now a well-formed type, though there must be an 
explicit ApplyTagT constructor for constructing dependent pairs.

Li-yao

On 9/9/2021 11:55 AM, Oleg Grenrus wrote:
> 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?
>>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>