[Haskell-cafe] Need help with advanced type-level programming

[Ximin Luo]

Ximin Luo:
> [..]
> 
> As for your code below, it would be easier if you try to describe what specifically you were stuck on, what were you trying to do. When you tried to write your function converting a TagList into a TagSet, what type signature are you expecting? It may be that the signature you thought you need, doesn't fit well into how you've expressed the rest of your data types.
> 
> [..]

Ah, it was simpler than I expected, although I suspect you'll want to write more complex things.

I first made the following tweak:

 SCon :: ((ht < mt) ~ True) => Tag con ht -> TagSet con (mt ': ts) -> TagSet con (ht ': mt ': ts)

Then listToSet can be written something like this:

listToSet :: forall con ss. TagList con ss -> Either String (TagSet con ss)
listToSet LNil = Right SNil
listToSet (LCon t LNil) = Right $ SSin t
listToSet (LCon t0@(Tag :: Tag con s0) tail@(LCon (Tag :: Tag con s1) _)) = case sing @s0 %< sing @s1 of
  STrue -> SCon t0 <$> listToSet tail
  SFalse -> Left "not ordered"

This uses some singleton typeclasses (POrd/SOrd), so you'll have to import the following:

{-# LANGUAGE ConstraintKinds, DataKinds, GADTs, PolyKinds, RankNTypes, ScopedTypeVariables, TypeApplications, TypeOperators #-}

import GHC.TypeLits
import Data.Kind
import Data.Singletons (Sing, sing)
import Data.Singletons.Prelude (SBool(..))
import Data.Singletons.Prelude.Ord (POrd(..), SOrd(..))

POrd for Symbol is actually defined in terms of CmpSymbol so you might be able to get your original code to work, but I couldn't after about 5 minutes of trying. This way is visually more consistent with other singletons code, though.

To write it in a more conventional singletons manner (as I understand; perhaps someone else will correct me) you can define Tag like so:

 Tag :: con s => Sing s -> Tag con s

which allows us to drop the KnownSymbol s constraint, and use these singletons directly later, instead of type-applications on `sing`:

listToSet (LCon t0@(Tag s0) tail@(LCon (Tag s1) _)) = case s0 %< s1 of

HTH

X

-- 
GPG: ed25519/56034877E1F87C35
GPG: rsa4096/1318EFAC5FBBDBCE
https://github.com/infinity0/pubkeys.git