Generate additional constructors with SingI constraints

[Icelandjack]

The original formulation generated SingRep constraints in eg successor branch

data N = O | S N

data instance 
  Π (n::N) where 
  SO :: Π O
  SS :: SingRep m => Π m -> Π (S m)

Currently it doesn't

data instance 
  Π (n::N) where 
  SO :: Π O
  SS :: Π m -> Π (S m)

But TH could generate those constructors as well

gen :: Π (a::k) -> (Π a, Dict (SingI a))
gen sing = (sing, withSingI sing Dict)

pattern SS_ :: () => (S n ~ sn, SingI n) => Π n -> Π sn
pattern SS_ n <- SS (gen -> (n, Dict))
  where SS_ n =  SS n

[Icelandjack]

So we don't have to pick a single answer to the ‘NATTY-in-Natty Question’

[RyanGlScott]

I'm lost here. To help put things into context for me: SingRep is no longer a thing in modern singletons, having been superseded by the SingKind class. It looks like from your terse code snippet that when you refer to "SingRep", you really have SingI on the brain, so I'll operate under that assumption.

Having said that: what benefit do you get from bundling SingI dictionaries existentially with Sing constructors? In other words, why does SS not suffice for your use cases?

[goldfirere]

I perhaps know more of the history here. Originally, the SS constructor packed both the implicit inner singleton and the explicit one. This worked nicely, but it means that datastructures took exponentially more space than they needed to. Then, I learned about how to implement withSingI (using unsafeCoerce). Despite its unsavory nature, an exponential speedup seemed worthwhile, and so I made the change not to pack implicit singletons inside of constructors. However, the change means that users have to explicitly use withSingI if they want an implicit singleton.

@Icelandjack is proposing here to have a pattern synonym behave like the constructor of old, but without storing the implicit singletons -- generating them on the fly. This might be sensible.

Perhaps a better question is this: if a user uses SS_ but doesn't actually need the implicit singleton, is there a performance penalty (after optimizing)? If not, then perhaps SS_ should be the recommended pattern and get the better name (i.e. without the underscore). Then, everyone would have easier access to implicit singletons at no runtime cost.

[RyanGlScott]

Ah, that explanation clears things up nicely, thanks.

That being said, I would be quite shocked if GHC were smart enough to optimize away all of this explicit dictionary-passing. As evidence, in this simple example:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Bug where

import Data.Constraint
import Data.Nat
import Data.Singletons.Prelude
import Data.Type.Equality

gen :: Sing (a :: k) -> (Sing a, Dict (SingI a))
gen sing = (sing, withSingI sing Dict)

pattern SS_ :: () => forall n. (S n ~ sn, SingI n) => Sing n -> Sing sn
pattern SS_ n <- SS (gen -> (n, Dict))
  where SS_ n =  SS n

f :: Sing (n :: Nat) -> n :~: n
f SZ      = Refl
f (SS sx) = case f sx of Refl -> Refl

If we compile f above (using the SS constructor, not the SS_ pattern synonym) we get the following Core:

Rec {
-- RHS size: {terms: 18, types: 45, coercions: 13, joins: 0/0}
Bug.$wf [InlPrag=[0], Occ=LoopBreaker]
  :: forall (n :: Nat). Sing n -> (n :: Nat) GHC.Prim.~# (n :: Nat)
[GblId, Arity=1, Caf=NoCafRefs, Str=<S,1*U>]
Bug.$wf
  = \ (@ (n_s4Ce :: Nat)) (w_s4Cf :: Sing n_s4Ce) ->
      case w_s4Cf
           `cast` (Data.Nat.D:R:SingNatz0[0] <n_s4Ce>_N
                   :: (Sing n_s4Ce :: *) ~R# (Data.Nat.R:SingNatz n_s4Ce :: *))
      of {
        SZ $d~_a4e3 ->
          case GHC.Types.HEq_sc
                 @ Nat
                 @ Nat
                 @ n_s4Ce
                 @ 'Z
                 ($d~_a4e3
                  `cast` (Data.Type.Equality.N:~[0] <Nat>_N <n_s4Ce>_N <'Z>_N
                          :: ((n_s4Ce :: Nat) ~ ('Z :: Nat) :: Constraint)
                             ~R#
                             ((n_s4Ce :: Nat) ~~ ('Z :: Nat) :: Constraint)))
          of cobox_a4fa [Dmd=<L,A>]
          { __DEFAULT ->
          CO: <n_s4Ce>_N
          };
        SS @ n1_a4e8 $d~_a4e9 sx_a3uE ->
          case GHC.Types.HEq_sc
                 @ Nat
                 @ Nat
                 @ n_s4Ce
                 @ ('S n1_a4e8)
                 ($d~_a4e9
                  `cast` (Data.Type.Equality.N:~[0] <Nat>_N <n_s4Ce>_N <'S n1_a4e8>_N
                          :: ((n_s4Ce :: Nat) ~ ('S n1_a4e8 :: Nat) :: Constraint)
                             ~R#
                             ((n_s4Ce :: Nat) ~~ ('S n1_a4e8 :: Nat) :: Constraint)))
          of cobox_a4fe [Dmd=<L,A>]
          { __DEFAULT ->
          case Bug.$wf @ n1_a4e8 sx_a3uE of ww_s4Ci [Dmd=<L,A>]
          { __DEFAULT ->
          CO: <n_s4Ce>_N
          }
          }
      }
end Rec }

But if we change f to use SS_ instead, we incur another call to HEq_sc in the resulting Core:

Rec {
-- RHS size: {terms: 22, types: 56, coercions: 18, joins: 0/0}
Bug.$wf [InlPrag=[0], Occ=LoopBreaker]
  :: forall (n :: Nat). Sing n -> (n :: Nat) GHC.Prim.~# (n :: Nat)
[GblId, Arity=1, Caf=NoCafRefs, Str=<S,1*U>]
Bug.$wf
  = \ (@ (n_s4BX :: Nat)) (w_s4BY :: Sing n_s4BX) ->
      case w_s4BY
           `cast` (Data.Nat.D:R:SingNatz0[0] <n_s4BX>_N
                   :: (Sing n_s4BX :: *) ~R# (Data.Nat.R:SingNatz n_s4BX :: *))
      of {
        SZ $d~_a4eD ->
          case GHC.Types.HEq_sc
                 @ Nat
                 @ Nat
                 @ n_s4BX
                 @ 'Z
                 ($d~_a4eD
                  `cast` (Data.Type.Equality.N:~[0] <Nat>_N <n_s4BX>_N <'Z>_N
                          :: ((n_s4BX :: Nat) ~ ('Z :: Nat) :: Constraint)
                             ~R#
                             ((n_s4BX :: Nat) ~~ ('Z :: Nat) :: Constraint)))
          of cobox_a4xs [Dmd=<L,A>]
          { __DEFAULT ->
          CO: <n_s4BX>_N
          };
        SS @ ipv_s4zN ipv1_s4zO ipv2_s4zP ->
          case GHC.Types.HEq_sc
                 @ Nat
                 @ Nat
                 @ n_s4BX
                 @ ('S ipv_s4zN)
                 (ipv1_s4zO
                  `cast` (Data.Type.Equality.N:~[0] <Nat>_N <n_s4BX>_N <'S
                                                                          ipv_s4zN>_N
                          :: ((n_s4BX :: Nat) ~ ('S ipv_s4zN :: Nat) :: Constraint)
                             ~R#
                             ((n_s4BX :: Nat) ~~ ('S ipv_s4zN :: Nat) :: Constraint)))
          of cobox_a4ep
          { __DEFAULT ->
          case GHC.Types.HEq_sc
                 @ Nat
                 @ Nat
                 @ ('S ipv_s4zN)
                 @ n_s4BX
                 (ipv1_s4zO
                  `cast` (Data.Type.Equality.N:~[0] <Nat>_N cobox_a4ep (Sym
                                                                          cobox_a4ep)
                          :: ((n_s4BX :: Nat) ~ ('S ipv_s4zN :: Nat) :: Constraint)
                             ~R#
                             (('S ipv_s4zN :: Nat) ~~ (n_s4BX :: Nat) :: Constraint)))
          of cobox1_a4xw [Dmd=<L,A>]
          { __DEFAULT ->
          case Bug.$wf @ ipv_s4zN ipv2_s4zP of ww_s4C1 [Dmd=<L,A>]
          { __DEFAULT ->
          CO: <n_s4BX>_N
          }
          }
          }
      }
end Rec }

This would certainly blow up in larger examples. As a result, I don't think I'd be quite ready to endorse the pattern synonym approach as the recommended one.

Another issue we'd have to worry about is that we'd presumably want to generate COMPLETE sets (e.g., {-# COMPLETE SZ_, SS_ #-}), but due to Trac #14059, they wouldn't actually kick in.

To summarize: I wouldn't be opposed to generating these, provided that:

1. We come up with a sensible naming convention (I'm not fond of SS_, since that prevents you from singling a constructor named S_).
2. We advertise the shortcomings of these pattern synonyms in the Haddocks.

[goldfirere]

Thanks for that very helpful analysis @RyanGlScott . I agree completely with the two conclusions at the end of his post.

[RyanGlScott]

On second thought, I'm going to say that this is something which belongs outside of singletons. My reasoning is:

1. We have to pollute the namespace with extra constructors suffixed with _, which is questionable at best.
2. This is quite easy to implement outside of singletons. As a proof of concept, I have a gist here that defines a genSingConstrained function which, given a Template Haskell Name, generates the corresponding pattern synonyms you've proposed. And it's less than 100 lines of code!

In short, I think this deserves to be its own library.

[Icelandjack]

The choice of _ was arbitrary, my only concern about 2. is ‘did the library author remember to derive the _ variant’ but that's fine

[RyanGlScott]

Luckily, this feature does not require generating orphan instances of any kind, so it's completely possible (and acceptable) to have singletons for a datatype and the corresponding pattern synonyms defined in separate locations. (Thus, if a library author doesn't define these pattern synonyms, it's quite possible to do so yourself without remorse.)