Using a non fully saturated type family
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? -- Rubén. (pgp: 4EE9 28F7 932E F4AD)
You cannot without a hacks until https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0242-un... 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-Sigm... 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?
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-un... 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-Sigm... 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.
On 09-09-21 12:00, Li-yao Xia wrote:
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.
This is a great hack! -- Rubén. (pgp: 4EE9 28F7 932E F4AD)
participants (3)
-
Li-yao Xia -
Oleg Grenrus -
Ruben Astudillo