The following gets stuck

newtype C (k :: AHyperType) = C (D k)
newtype D k = D (C k)

makeHTraversableApplyAndBases ''D
makeHTraversableApplyAndBases ''C

This is probably due to the instances somehow "flattening" the infinite structure.

Hi,

I was not able to find hypertypes package on hackage.
Is it on purpose or just published under different name?

recursiveContexts is currently limited to annotated expressions, can it be generalized?

Take for example, this language of literals, type-annotated expressions and
kind annotated types.

data Expr h
  = ExprLit Int
  | -- | ExprAdd (h :# Expr) (h :# Expr)
    ExprAnn (h :# Expr) (h :# Type)
  deriving stock (Generic)

data Type h
  = TypeUnit
  | TypeAnn (h :# Type) (h :# Kind)

type Kind :: AHyperType -> Data.Kind.Type
data Kind h
  = KindStar

makeHNodes ''Expr
makeHFunctor ''Expr
makeHNodes ''Type
makeHFunctor ''Type
makeHNodes ''Kind
makeHFunctor ''Kind
instance RNodes Expr
instance RNodes Type
instance RNodes Kind
instance (c Kind) => Recursively c Kind
instance (c Kind, c Type) => Recursively c Type
instance (c Kind, c Type, c Expr) => Recursively c Expr

If we want to perform a fold over an Expr we have to do a little dance with
HRecWitness, deconstructing it recursively.

showE' :: Pure # Expr -> String
showE' = fold \case
  HRecSelf -> \case
    ExprLit i -> show i
    ExprAnn (Const e) (Const t) -> e <> " : " <> t
  HRecSub (HWitness W_Expr_Expr) HRecSelf -> \case
    ExprLit i -> show i
    ExprAnn (Const e) (Const t) -> e <> " : " <> t
  HRecSub (HWitness W_Expr_Type) HRecSelf -> \case
    TypeUnit -> "()"
    TypeAnn (Const t) (Const k) -> t <> " : " <> k
  ...

One can mechanically derive a GADT representing the closure of the HWitness
relation, which makes defining these folds much more pleasant:

withWitnessClosure
  :: forall e t p a
   . (Recursively (WitnessClosure e) e)
  => (HWitnessClosure e t -> t # p -> a)
  -> HRecWitness e t
  -> t # p
  -> a
withWitnessClosure f = Proxy @(WitnessClosure e) ##>> f inClosure

type WitnessClosure :: HyperType -> HyperType -> Constraint
class WitnessClosure e t where
  inClosure :: HWitnessClosure e t

instance WitnessClosure Expr Expr where inClosure = E
instance WitnessClosure Expr Type where inClosure = T
instance WitnessClosure Expr Kind where inClosure = K

type HWitnessClosure :: HyperType -> HyperType -> Data.Kind.Type
data family HWitnessClosure a b
data instance HWitnessClosure Expr a where
  E :: HWitnessClosure Expr Expr
  T :: HWitnessClosure Expr Type
  K :: HWitnessClosure Expr Kind

-- Used thusly:
showE :: Pure # Expr -> String
showE =
  fold
    ( withWitnessClosure \case
        E -> \case
          ExprLit i -> show i
          ExprAnn (Const e) (Const t) -> e <> " : " <> t
        T -> \case
          TypeUnit -> "()"
          TypeAnn (Const a) (Const b) -> a <> " : " <> b
        K -> \case
          KindStar -> "*"
    )

Does this construct have a place in hypertypes, or is this actually quite an
unidiomatic way of performing such a fold?

It seems like defining a Showable class and writing instances for Expr,
Type and Kind might be the "proper" way to go? Something like:

type Showable :: HyperType -> Constraint
class Showable h where
  show' :: h # Const String -> String

instance Showable Expr where
  show' = \case
    ExprLit i -> show i
    ExprAnn (Const e) (Const t) -> e <> " : " <> t

instance Showable Type where
  show' = \case
    TypeUnit -> "()"
    TypeAnn (Const a) (Const b) -> a <> " : " <> b

instance Showable Kind where
  show' = \case
    KindStar -> "*"

showE' :: Pure # Expr -> String
showE' = fold $ Proxy @Showable ##>> show'

This issue is about the ability to implement languages with type-classes. Such that LangB will have another term constructor BInstance which evaluates to a type-class instance according to its type (such as [Int] -> Json).

• The infer of "instance" nodes should add a type-class constraint
  • For evaluation/compilation: it might be useful for the InferOf to include a reference to the term's corresponding type-class constraint so that the type-class instance can be looked up from it
• The generated constraints can probably be resolved/simplified in a post-process after the inference, that matches them with existing instances. For example [Int] -> Json can be resolved by a -> Json => [a] -> Json and Int -> Json.
• TODO (flesh-out): We should consider the interactions with let-generalization and to-nom

We currently use the GetHyperType type family to unwrap 'AHyperTypes, but Haskell doesn't currently understand that it's a bijective type family so it doesn't infer that trees are always of shape k0 (`HyperType k1) and this leads to less helpful type errors and sometimes requires extra type signatures or usage of the asHyper inference-assisting identity function.

Using GADTs instead of TypeFamilies would provide better error messages. But transitioning to them is problematic because:

• Generic derivation for GADTs doesn't work
• lens TH code doesn't always work for GADTs
• Our own TH derivations need to be augmented to support GADTs

We currently have the HasChild class for node lens. Data types a la carte has the :<: type class for injections (can be generalised to prisms) and we have specific cases for it like HasFuncType. We should create a unified class for optics to nodes, but the contexts of optics are somewhat complicated so we'll keep it in an issue for now.

It's hidden away in Hyper.Internal.Prelude but it seems like it could just be exported, and it'd useful!

In the following example:

newtype A i k = A (B i k)
newtype B i k = B (i (k :# A i))

makeHNodes ''A
makeHNodes ''B
makeHFunctor ''A
makeHFunctor ''B

makeHFunctor ''B correctly adds the Functor i context, but makeHFunctor ''A does not.

makeHFunctor should accept a list of co-recursive types, and be able to resolve the right context for each instance.
And same is true for other TH derivations.

I was re-reading the README to try to refresh my understanding, and noticed a couple of probable editing snafus:

• At one point, there is the sentence: "Some extensions we use but would like to avoid (we're looking for alternative solutions but haven't found them):", but then there is nothing following the colon.

• A bit further down, "one would have to declare an explicit expression type for each expression type for use as ...". Was a sentence fragment accidentally duplicated here? (If not, maybe it's just a bit confusing.)

And something I started wondering about: how does the hypertypes approach compare to the "HKD for nested structures" approach?

The only listed drawback of the latter is that Rank2.Functor doesn't work for it. Ok. (Could you write a separate class?) But apart from that...

data Expr f
    = EVar Text
    | EApp (f (Expr f)) (f (Expr f))
    | ELam Text (f (Typ f)) (f (Expr f))

data Typ f
    = TInt
    | TFunc (f (Typ f)) (f (Typ f))

It does seem to handle mutual recursion fine (at least, as far as writing down the types). And the two seem kind of analogous in a way: in one case, you have f on the outer level and the recursive structure is again parameterized by f; and in the other, you have h on the outer level, which, internally, applies its parameter (e.g. Expr) to h again to achieve parameterization of the recursive structure.

If I were to hazard a very rough guess, maybe the HKD approach is fine as long as you only want to alter the shape in "regular" ways, in some sense, while hypertypes in addition lets you do fancy tricks with the underlying fixpoints...?

As mentioned in #17 it might be beneficial to split up hypertypes into several individual packages.

The AST+Inference+Unification could certainly be split off into a separate package (leaving hypertypes as just the main data structure and generic machinery/classes), whether to split that further is probably a matter of taste. Certainly there do exist other packages which solely deal with unification, for example.

• Scheme
• LangA

example:

newtype A a (h :: AHyperType) = A (a h)
newtype B a (h :: AHyperType) = B (A a h)

makeHTraversableAndBases ''A
makeHTraversableAndBases ''B

results in

instance HNodes (B a_aiop) where
  type forall constraint. HNodesConstraint (B a_aiop) constraint = Solo
                                                                   HNodesConstraint a_aiop constraint
  type HWitnessType (B a_aiop) = W_B a_aiop
  {-# INLINE hLiftConstraint #-}
  hLiftConstraint (HWitness (E_B_a witness))
    = hLiftConstraint witness
data W_B (a_aiop :: AHyperType -> Type) node
  where E_B_a :: (HWitness a_aiop node) -> W_B a_aiop node
instance HFunctor a_aiop => HFunctor (B a_aiop) where
  {-# INLINE hmap #-}
  hmap _f (B x0)
    = B ((\case A x1 -> A ((hmap (_f . (HWitness . E_B_a))) x1)) x0)
instance HFoldable a_aiop => HFoldable (B a_aiop) where
  {-# INLINE hfoldMap #-}
  hfoldMap _f (B _x0)
    = (\case A _x1 -> (hfoldMap (_f . (HWitness . E_B_a))) _x1) _x0
instance HTraversable a_aiop => HTraversable (B a_aiop) where
  {-# INLINE hsequence #-}
  hsequence (B _x0) = (pure B <*> hsequence _x0)

unlike the other classes, there is no HNodes a constraint for the HNodes (B a) instance, and the code doesn't compile, with Could not deduce (HNodes a)

Hello; thanks for this lovely library!

I'm trying to wrap my mind around it.

In the README, you start with a Person example; but then quickly jump into ASTs.

My usage isn't actually an AST; it's much more like the Person example. I'm here because I couldn't quite get barbies to work ( see jcpetruzza/barbies#47 ).

In my own hacking, I'm trying something like

data Person h = Person
    { height :: h :# Const Double
    , weight :: h :# Const Double
    , name   :: h :# Const Text
    }

person :: Pure # Person
person = Pure $ Person
  { height = Pure $ Const 5.0
  , weight = Pure $ Const 1.0
  , name   = Pure $ Const "name"
  }

maybePerson :: Maybe # Person
maybePerson = undefined

what's not clear to me is how to define the maybePerson type. As-is, it doesn't compile. I think I need to somehow adapt the Maybe type to be a kind of Hyper type; but I'm missing exactly how.

I'd love to know how to do this; and then do barbie-style things such as a bmap which takes, say, an Identity # Person and converts it to a Maybe # Person via runIdentity.

Thanks!

The version on there is ~2 years old by now :)

On a similar note, and I don't mean this to sound flippant, but how would you feel about splitting up the package into some smaller pieces. At the moment it's very easy to look at it and see hypertypes as an ecosystem to buy into, but the "core" could be very neatly separated from the AST/Infer/Unify side of things, and would perhaps be an easier pick for those looking for "recursion schemes, but for mutually recursive datatypes".

This is,of course not a project I've contributed to yet and there are benefits to having a monoproject!

I was playing around with the release on stackage and running into missing modules problem (Hyper.Syntax.App and others) which was me looking at the HEAD version and using version 0.1.0.2 release. Unfortunately, there are no release tags which makes it difficult to browse the code for the release. It would be very helpful if you could tag the repo when you release new versions.

Thank you! Looking forward to using hypertypes.