The lack of documentation makes it hard to navigate

[Mikolaj]

How does this relate to https://hackage.haskell.org/package/first-class-families? It seems to have a similar module hierarchy, but what's the relation?

What's the goal?

How to use it?

Which parts are complete, which are WIP?

[rybochodonezzar]

The idea was to be able to represent fcf's type level functions on term level Given fcf's data Foo :: a -> Exp b it can be expressed on term level as foo :: ta x-> SExp tb (Foo x) where

ta :: a -> *
tb :: b -> *
newtype SExp t a = SExp { eval :: t (Eval a) }

So this is general purpose, but my particular goal was to later implement extensible record with fcf, and use this for fine grained typed validation and queries on arbitrary data

Class.Foldable is only unfinished module for now

Regarding lack of doc: i planned to document it once i finish implementation, but i wasn't sure how much documentation is necessary here, since most functions simply reflect their fcf counterparts, i think only Core module needs explanation

[Mikolaj]

Oh, fsf counterparts? That's a precious hint. Which function is a counterpart of which fcf function? Are modules counterparts as well, or do I need to track individual functions to their counterparts?

[rybochodonezzar]

Modules are counterparts. For every fcf function Foo it's counterpart is called fooS, and for every operator there is a counterpart prefixed with &

[Mikolaj]

Oh, nice and indeed a type-level function in fsf corresponds to a value-level function in fsf-singletons. And, presumably, the original types can be recovered via singletons? But fsf has higher-order type functions, can singletons recover that? Does it require some fancy or questionable GHC extensions? Is there a nice commuting diagram showing that if you apply functions in fsf-singletons and read the type via singletons, you get the same (or something isomorphic? what's the isomorphism) to reading first and evaluating in fsf?

i'm asking a lot of question in particular because the answer to these would probably make for sensible starting documentation of your package. Publishing version 0.0.0.1 (or at least a Hackage candidate) would also help by making haddocks available.

Are there any tests of your package that also demonstrate how one uses it and, in addition, demonstrate what the benefit of the package is? Ideally, the tests would be gathered in a test section of the .cabal file and run by GHA.

[rybochodonezzar]

But fsf has higher-order type function, can singletons recover that? I'm not exactly sure what do you mean by recover. It is possible to represent fcf's higher order functions on as functions on singletons, for example:

class FunctorS f where
fmapS :: (forall x . t1 x -> SExp t2 (r x)) -> f t1 a -> SExp (f t2) (FMap r a)

If by recover you mean something else, please clarify

Is there a nice commuting diagram showing that if you apply functions in fsf-singletons and read the type via singletons, you get the same (or something isomorphic? what's the isomorphism) to reading first and evaluating in fsf?

That's the point of it, but i'm not as strong in CT as to provide a diagram for it. The case of reading first, then evaluating in fcf is only possible when you evaluate to fully monomorphic type, which is only realistic in tests, otherwise you'd rather want to know that output of your function corresponds to output of type level fcf function for any input

Regarding tests, at minimum i'll replicate fcf tests once all components are finished, which will also show how many fancy extensions are needed on user side. There is also possibility of some stronger, QuickChekc based tests later.

[Mikolaj]

I also mean a demo that shows "foo can almost be done by fcf (or some other libraries), but not quite, and fcf-singletons can do it fine like that:...".

BTW, I've just learned that "reflect" and "reify" are inverses. Does fcf-singletons somehow reflect the types created by fcf and fcf somehow reify Haskell value expressions? Or, in addition to being imprecise, is this beside the point?

Also, if I have a simple Haskell expression e, move it to type level with fcf (how?), then back to value level with fcf-singletons, what's the relation of the result with the original e? Why don't I just use e?