Feature request, custom Typeable?

oliver-batchelor commented 7 years ago

It seems that even though Typeable is not compulsory, and the decorator method is also supported for closed type domains - it seems to creep into a lot of the features of syntactic, could something generalizing the Typeable interface work?

class Typed rep a where typeRep :: proxy a -> rep a

data BindingT rep sig where VarT :: Typed rep a => Name -> BindingT (Full a)
LamT :: Typed rep a => Name -> BindingT (b :-> Full (a -> b))

Edit: Given that there're papers written on syntactic < 2.0, it would be nice to get a good overview of what the major differences are with the latest versions.

emilaxelsson commented 7 years ago

Sorry for the delay!

I think it's a good suggestion to parameterize on the type representation. I'm no longer working at the university, so I can't spend time on this. But I'm happy to accept patches, and can also give guidance if needed.

Regarding the various versions, here is the short story:

Syntactic-1.* had a lot of experimental stuff, some of which I wasn't very happy with. I bumped the major version when the paper was published, but it should really have stayed at 0.* until things settled.
In Syntactic >= 2 I cleaned up the library and kept only the things I was happy with. I'm not aware that anyone but me used those things anyway. I also moved away from HOAS (which worked very badly together with the rest of Syntactic) and went for the circular first-order approach currently used.

As a result the current library is lacking some things that would be nice to have and that it was originally intended to have (e.g. observable sharing), but at least the things that are there work rather well I think.

oliver-batchelor commented 7 years ago

Thanks a lot for the reply! I didn't actually notice you'd replied, sorry! Since I first posted that up I've become much more familiar with what's going on and appreciate some more of the subtleties.

I'm quite interested in the idea that @Icelandjack had, it seems like the most straightforward way to include closed type Universes, do you have any idea what happened to that - was it stuck on a GHC Issue?

emilaxelsson commented 7 years ago

I'm not sure. I don't think the GHC issue was a blocker, since he posted a less general workaround.

oliver-batchelor commented 7 years ago

Hmm - the problem with the restricted AST type is that you lose the closed type Universe again (which I guess is the main benefit).

Btw. I have been playing with a type

data SumF :: [k -> Type] -> k -> Type where
   L :: f a -> SumF (f : fs) a
   R :: SumF fs a -> SumF (f : fs) a

https://gist.github.com/Saulzar/d863a15cd0c122a4ffa8655d9e8ce81f

which seems to let you do most of the same things as (:+:) but without overlapping types, do you know of any downside to this kind of type?

emilaxelsson commented 7 years ago

That looks like a nice approach. I think with a list it gets harder to do composing and decomposing of domains as in Composing and decomposing data types: a closed type families implementation of data types à la carte.

But compared to the original Data Types à la Carte, used in Syntactic, I cannot think of any downsides of your approach. Possibly the type errors get worse...

Where do modules like Type.Family.List come from?

oliver-batchelor commented 7 years ago

Mostly from type-combinators https://hackage.haskell.org/package/type-combinators, there may be a couple of extraneous imports in that gist. Most useful is the class Elem from Data.Type.Index

emilaxelsson / syntactic

Feature request, custom Typeable? #30