SChecked for gradual typing.

[tscholak]

Hi, @jul1u5 and I are trying to manually write a special singleton data type for gradually typed hasktorch.

We'd like a generic singleton datatype, SChecked a, that makes it possible to encode two situations:

1. a is a singleton type itself and therefore checked by the compiler. For instance, a could be SNat or SBool.
2. a is just a type like Natural or Bool and therefore unchecked by the compiler.

The nice thing about this is that values of type SChecked a can just be passed around like every other (singleton) value, and one can write programs that work with both forms of inputs, checked or unchecked. This is a huge convenience and makes it possible to gradually introduce stronger types.

We already have had success with specialized singleton types that distinguish between the two cases, see, e.g., https://github.com/hasktorch/hasktorch/blob/7bec8c01e85aa5ebf618f27122e88f50b5c75109/experimental/gradually-typed/src/Torch/GraduallyTyped/Layout.hs#L67, but we would like to have a more generic solution.

We have come up with the following encoding for SChecked a:

type Checked :: Type -> Type -> Type
data Checked a b = Checked a | Unchecked b

type SChecked :: Checked a Type -> Type
data SChecked checked where
  SUnchecked :: forall b. b -> SChecked @b ('Unchecked b)
  SChecked :: forall k a. Sing a -> SChecked @k ('Checked a)

type instance Sing = SChecked

instance (SingKind a, Demote a ~ a) => SingKind (Checked a Type) where
  type Demote (Checked a Type) = Checked a a
  fromSing (SUnchecked a) = Unchecked a
  fromSing (SChecked a) = Checked (fromSing a)
  toSing (Unchecked a) = SomeSing (SUnchecked a)
  toSing (Checked a) = withSomeSing a $ SomeSing . SChecked

This works, but the hidden kind annotation @b is a bit clumsy,

foo :: SChecked ('Checked 4)
foo = SChecked (SNat @4)

bar :: SChecked @Bool ('Unchecked Bool)
bar = SUnchecked True

We were wondering if someone has a better idea. Thanks!

[goldfirere]

What you really want is this, I think:

type Checked :: Type -> Type
data Checked a where
  Checked :: a -> Checked a
  Unchecked :: forall b -> Checked b

That is, 'Unchecked should take the name of the checked type, not an element of the checked type. But we don't have this yet -- soon. (See https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0402-gadt-syntax.rst) So here are two approximations:

type Checked :: Type -> Type
data Checked a where
  Checked :: a -> Checked a
  Unchecked :: Proxy b -> Checked b

-- This is just to appease the injectivity check on Demote
type Unchecked :: Type -> Type
newtype Unchecked a = MkUnchecked { unUnchecked :: a }

type SChecked :: Checked a -> Type
data SChecked checked where
  SUnchecked :: forall b. b -> SChecked @b ('Unchecked 'Proxy)
  SChecked :: forall k a. Sing a -> SChecked @k ('Checked a)

type instance Sing = SChecked

instance (SingKind a, Demote a ~ a) => SingKind (Checked a) where
  type Demote (Checked a) = Unchecked (Demote a)
  fromSing (SUnchecked a) = MkUnchecked a
  fromSing (SChecked a) = MkUnchecked (fromSing a)
  toSing (MkUnchecked a) = withSomeSing a $ SomeSing . SChecked

foo :: SChecked ('Checked 4)
foo = SChecked (SNat @4)

bar :: SChecked ('Unchecked @Bool 'Proxy)
bar = SUnchecked True

A key step here is using a different type (Unchecked) for the unrefined version of Checked. (I don't see why we need the Checked vs Unchecked distinction after calling fromSing... but even if we do, it needn't be the type called Checked.) Those 'Proxys are annoying. So here is another version:

type Checked :: Type -> Type
data Checked a where
  Checked :: a -> Checked a
  Unchecked :: forall b. Checked b

-- This is just to appease the injectivity check on Demote
type Unchecked :: Type -> Type
newtype Unchecked a = MkUnchecked { unUnchecked :: a }

type SChecked :: Checked a -> Type
data SChecked checked where
  SUnchecked :: forall b. b -> SChecked ('Unchecked @b)
  SChecked :: forall k a. Sing a -> SChecked @k ('Checked a)

type instance Sing = SChecked

instance (SingKind a, Demote a ~ a) => SingKind (Checked a) where
  type Demote (Checked a) = Unchecked (Demote a)
  fromSing (SUnchecked a) = MkUnchecked a
  fromSing (SChecked a) = MkUnchecked (fromSing a)
  toSing (MkUnchecked a) = withSomeSing a $ SomeSing . SChecked

foo :: SChecked ('Checked 4)
foo = SChecked (SNat @4)

bar :: SChecked ('Unchecked @Bool)
bar = SUnchecked True

The downside here is that the argument to 'Unchecked must always be preceded by @. A bit annoying, but also very formulaic once you know to expect it. Or, it can be plastered over with this:

type UncheckedV :: forall b -> Checked b
type UncheckedV b = 'Unchecked @b

Does this look like it would work better in your use case?

[tscholak]

Hi @goldfirere, thank you for this very detailed response and the great ideas!
I think I like version 2 (without Proxy) better.
A small issue is that the Haskell Language Server doesn't show the @ annotation, and also doesn't add it to automatically generated type signatures, e.g. for bar. Not sure if this a matter of configuration.

I don't see why we need the Checked vs Unchecked distinction after calling fromSing...

Maybe it's a bit pedantic, but I wanted to make a lawful SingKind instance with 'toSing' . 'fromSing' ≡ 'SomeSing', and I think that requires that we keep this distinction around at the value level.

[goldfirere]

Hard to know whether that identity would be important -- but I appreciate your interest in upholding it. In any case, even if you want to remember the checked-status after calling fromSing, you can add a second constructor to Unchecked, while still keeping the overall scheme.