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

[Ximin Luo]

Hi Evgeny,

I've gotten into this topic recently myself and have a few broad tips, that you might find useful. My first comment is that what you seem trying to do below is non-trivial, and might well take a few days or a week if this is the first time trying to do it - it did for my first piece of non-trivial type-level code. So don't try to rush into it, try to understand the background first with some more simple examples.

- Are you aware of the singletons library? It makes life a lot easier. There is a nice introductory series of posts here: https://blog.jle.im/entry/introduction-to-singletons-1.html There are 4 parts and together they will take a couple of days to sink in.

- This is a nice talk https://www.youtube.com/watch?v=wNa3MMbhwS4 with a clarifying example near the end on how to write proofs as constraints.

- `constraints` is a library that lets you wrap constraints so you can pass instances manually around, e.g. generate an instance in a utility function (i.e. prove a theorem), and then return it so the caller can use it.

- Always switch on PolyKinds, and be prepared to use TypeApplications a lot

- case-matching on GADTs is important for GHC to deduce certain things, and this only works on the RHS of a pattern match. Sometimes it can be important to match on constructors of GADTs even if the values are unused on the term-level - this can mean the difference between a type error and no type error. And `let Pattern = ..` didn't seem to work for me at least in some cases, it had to be a `case`.

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.

X

Evgeny Permyakov:
> Consider following code
> 
> data Tag :: (Symbol -> Constraint) -> Symbol -> * where
>  Tag :: (KnownSymbol s, con s) => Tag con s
> 
> data TagList :: (Symbol -> Constraint) -> [Symbol] -> * where
>  LNil :: TagList con '[]
>  LCon :: Tag con s -> TagList con ss -> TagList con (s ': ss)
> 
> data TagSet :: (Symbol -> Constraint ) -> [Symbol] -> * where
>  SNil :: TagSet con '[]
>  SSin :: Tag con s -> TagSet con '[s]
>  SCon :: CmpSymbol ht mt ~ LT => Tag con ht -> TagSet con (mt ': ts) -> TagSet con (ht ': mt ': ts)
> 
> How one would write a function converting a TagList into a TagSet , dropping duplicate tags ? I tried a few approaches, but failed. I clearly lack understanding how to fit it into GHC type system. I know there is a library  type-level-sets, but it isn't what I would like and I don't understand how it fits into GHC type system, so it appears to be magical to me.
> 
> Similarly, it would be greatly appreciated if someone could show how to implement following typeclass 
> 
> class CmpTag (s1 :: Symbol) (s2 :: Symbol) where
>  cmpTag :: Tag con s1 -> Tag con s2 -> OrdTag con (CmpSymbol s1 s2) s1 s2
> 
> data OrdTag :: (Symbol -> Constraint) -> Ordering -> Symbol -> Symbol -> *  where
>  TLT ::  CmpSymbol s1 s2 ~ LT           => Tag con s1 -> Tag con s2 -> OrdTag con LT s1 s2
>  TEQ :: (CmpSymbol s1 s2 ~ EQ, s1 ~ s2) => Tag con s  -> Tag con s2 -> OrdTag con EQ s1 s2
>  TGT ::  CmpSymbol s1 s2 ~ GT           => Tag con s1 -> Tag con s2 -> OrdTag con GT s1 s2
> 
> 
> _______________________________________________
> 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.
> 


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