search

FormationAI / dhall-bhat

Tasty meal of Dhall
66 stars 11 forks source link

Kind polymorphism #42

Closed sellout closed 5 years ago

sellout commented 5 years ago

Still very much in progress, with a lot of stuff commented out.

Also, currently requires the kind-polymorphism branch of dhall-haskell.

FintanH commented 5 years ago

Ok I didn't even make it half way. But my thought is that we should separate the abstractness out into its own home and dhall-bhat uses that lib to to concretise over Set.

I think this is a good move to allow people to easily reason about dhall-bhat without knowing a bunch of category theory. It will still look a bit strange when people do see it but we would heavily document it, likely with the normalised form that will look more familiar to people.

That way the separation of concerns is Set vs. other categorical implementation (if any?).

sellout commented 5 years ago

Yeah, I was thinking similarly. The nice thing is that normalization should make the specialized types for Set look very reasonable.