Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
A sketch of how we might single visible type applications
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TopLevelKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module SingletonsVTA where
import Data.Kind
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family (f :: a ~> b) @@ (x :: a) :: b
type Sing :: forall k. k -> Type
data family Sing
newtype instance Sing (f :: k1 ~> k2) =
SLambda { (@@) :: forall t. Sing t -> Sing (f @@ t) }
type SingFunction1 f = forall t. Sing t -> Sing (f @@ t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f
type SingFunction2 f = forall t. Sing t -> SingFunction1 (f @@ t)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))
data instance Sing :: forall a. [a] -> Type where
SNil :: Sing '[]
SCons :: Sing x -> Sing xs -> Sing (x:xs)
constBA :: forall b a. a -> b -> a
constBA x _ = x
type ConstBA :: forall b a. a -> b -> a
type family ConstBA x y where
ConstBA x _ = x
type ConstBASym0 :: forall b a. a ~> b ~> a
data ConstBASym0 x
type instance ConstBASym0 @@ x = ConstBASym1 x
type ConstBASym1 :: forall b a. a -> b ~> a
data ConstBASym1 x y
type instance ConstBASym1 x @@ y = ConstBA x y
sConstBA :: forall b a (x :: a) (y :: b).
Sing x -> Sing y -> Sing (ConstBASym0 @@ x @@ y :: a)
sConstBA sx _ = sx
blah :: forall b a. [a] -> [b -> a]
blah x = map (constBA @b) x
type Map :: forall a b. (a ~> b) -> [a] -> [b]
type family Map f xs where
Map _ '[] = '[]
Map f (x:xs) = (f @@ x) : Map f xs
sMap :: forall a b (f :: a ~> b) (xs :: [a]).
Sing f -> Sing xs -> Sing (Map f xs :: [b])
sMap _ SNil = SNil
sMap sf (SCons x xs) = (sf @@ x) `SCons` sMap sf xs
type Blah :: forall b a. [a] -> [b ~> a]
type family Blah x where
Blah @b x = Map (ConstBASym0 @b) x
type BlahSym0 :: forall b a. [a] ~> [b ~> a]
data BlahSym0 x
type instance BlahSym0 @@ x = Blah x
sBlah :: forall b a (x :: [a]). Sing x -> Sing (BlahSym0 @@ x :: [b ~> a])
sBlah sx = sMap (singFun2 @(ConstBASym0 @b) sConstBA) sx
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment