victorcmiraldo / generics-mrsop Goto Github PK

When a datatype occurs multiple times within another datatype,
multiple pattern synonyms are generated, leading to invalid haskell code

see b0818ae for triggering the bug

While reading the multirec paper again this weekend, I see that a shallow conversion is easier for the end-user to interface. Instead of that complicated 'crush' mess, one can define the standard compos
combinator

The meat of the change is in NA , where our recursive index changed from Nat -> * to [*] , and inside
the NA_I constructor we require a specific element of that list.

The Element class then becomes Family , where we require, explicitly, an element of the list of types and convert it to a representation. I believe I can write
a more elegant interface by having another class Element that matches on the ty and ix and
performs those injections into El ix fam automatically.

This is a scratchpad;

First instance: d4eb743#diff-d775fda351c2b2035857ec967d996b0aR108

elimRep :: (forall k. ki k -> a) -> (forall k. f k -> a) -> ([a] -> b) -> Rep ki f c -> b

should be:

elimRep :: (forall k. ki k -> a) -> (forall k. IsNat k => f k -> a) -> ([a] -> b) -> Rep ki f c -> b

just like elimRepM already is

hs-elisp commit working around it

When compiling the following code:

import Generics.MRSOP.TH
import Generics.MRSOP.Base
import Language.ELisp -- comming from hs-elisp

generateFamilyWith 'W [t| [ESExp] |]

I run into:

> ghc: panic! (the 'impossible' happened)
>   (GHC version 8.4.3 for x86_64-unknown-linux):
>         completeCall
>   fail_aeDS
>   Select nodup wild_00
>   Stop[BoringCtxt] Rep
>                      W (El FamListESExp) (Lkup ix_aeTL CodesListESExp)
>   Call stack:
>       CallStack (from HasCallStack):
>         callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
>         pprPanic, called at compiler/simplCore/Simplify.hs:1533:9 in ghc:Simplify
>
> Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

I want to make a small reproducible file before submitting it as a bug, though.

Now that we can do catamorphisms and paramorphisms over mutal recursive datatypes,
we actually have enough power to write an embedded DSL for Attribute Grammars.

@serras and I brainstormed a bit about this today.

Commit here: 835de82

Branch here: https://github.com/VictorCMiraldo/generics-mrsop/compare/arian-dev

Hide the documentation of the example modules

https://www.haskell.org/haddock/doc/html/module-attributes.html

https://github.com/VictorCMiraldo/generics-mrsop/blob/master/src/Generics/MRSOP/Base/NP.hs#L48

They can live with just an Applicative constraint. Perhaps to be consistent we should name them traverse instead of mapM as well

We need a lot of treefix functionality all over the place, and it seems this will be very useful
later on, on my lambda-world tutorial.

For this reason, we'll bring treefixes into generics-mrsop. Moreover, we will add annotations
to treefixes:

data TreefixAnn phi ki codes at

type Treefix = TreefixAnn () -- in Simple.hs

We do need synthetization of attributes for annotated treefixes in all four variants:

synthesizeTx
synthesizeTxAnn
synthesizeTxM
synthesizeTxAnnM

@arianvp and @serras ; I am done preparing this to Hackage; I'm just waiting to be put in the uploader group and I'll proceed uploading generics-mrsop-1.0.0.0 to hackage.

This means that the master branch has to be protected; If you want/need features and changes, please
for off master and make a pull request!

Cheers!

The title says it all... :P

I have prepared the writeup folder with a makefile, acmsmall style, lhs2tex and bibtex integration.

Running make there should generate a folder dist, where one will find the pdf.
I assume the setup is straight forward, but let me know if you have questions.

I think we should each make our own branch to edit our parts of the text. Call then writeup-victor and writeup-alejandro. We then make efforts to merge to writeup often. This should minimize
our trouble and keep a clear history of changes. What do you think?

It makes Pattern matching on Indexed Sums O(1) which will make our converisons a bit more efficient.

Also, it might fool the compiler into fixing #6
http://hackage.haskell.org/package/freer-effects-0.3.0.1/docs/Data-OpenUnion.html
http://hackage.haskell.org/package/freer-effects-0.3.0.1/docs/Data-OpenUnion-Internal.html

Name Holes accordingly with generics-simplistic

There's an interesting approach to get SOP universes from just a Generic instance. I think
we can use this as well?

http://hackage.haskell.org/package/generics-sop-0.3.2.0/docs/Generics-SOP-GGP.html#t:GCode

http://www.andres-loeh.de/GenericGenericProgramming

After reading Andres' comments, I have thought about changing the table slightly into the following form:

(the two rows for generics-mrsop should be combined, but Markdown in not LaTeX).

I would also move the paragraph which says:

Some functions really need the information
about which fields of a constructor are recursive and which are not,
like the generic |map| and the generic |Zipper|

even before the contributions so that the reader knows that deep representations are not just nice theoretically, there are also practical reasons to want them.

Comments?

example:

import Language.Lua.Syntax
deriveFamily [t| State |]

Error:

convertType: Unsupported Type: TupleT 2

I think support for this should be trivial to add right? Tuple should just become one
of the datatypes in the generated family.

As it turns out, using NS and NP from sop-core came with an annoying difficulty. The handling of typeclasses is more complicated than what it needs to be.

I think we need to use NS and NP from sop-core, granted. But we should restore
EqHO and ShowHO like before:

class EqHO f where
  eqHO :: f x -> f x -> Bool

This makes the treatment of typeclasses much easier for our particular context. One example
of a difficult scenario is in here, where we can't just use (==) because
sop-core's instance requires an instance of All (Compose Eq (NA ki (Fix ki codes))) (Lkup c sum), however, c here is a local type variable that comes from a call to sop.
Here's a smaller outline:

difficult :: Fix ki codes ix -> Bool
difficult x = case sop x of
                  Tag cx px -> px == px

The code above will not compile; We would need to propagate the All (Compose ...) constraint
to the Tag constructor to make it usable, and that's solely for Eq; if we need Eq and Show, then we'd need to propagate both constraints and so on and so forth.

@serras , do you know of a better alternative?

The EqHO approach we had before would allow a third party to easily provide typeclasses
working over generic code, this current approach is not so lightweight.

             
/home/arian/Documents/UU/Thesis/generics/generics-mrsop-diff/src/Examples/Lua.hs:9:1: error:
    GHC.Prim.ByteArray# is not a declaration
  |          
9 | deriveFamily [t| Stat |]
  | ^^^^^^^^^^^^^^^^^^^^^^^^

This error was due to the fact that Text from the text package is an ADT defined in terms of ByteArray# . How can I convince the deriveFamily machinery to pick it as an atom instead?

http://hackage.haskell.org/package/sop-core

Generics-sop has extracted all its utility functors like NS and NP to a separate package. Would be nice to use those versions.

GHC seems to hang when compiling GoAST.

There is a bug report here that might be relevant.

Taken from here

cataM' :: (Monad m , IsNat ix)
       => (forall iy a. IsNat iy => Fix ki codes iy -> m a -> m a)
       -> (forall iy  . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy))
       -> Fix ki codes ix
       -> m (phi ix)
cataM' p f xo@(Fix x) = mapRepM (p xo . cataM' p f) x >>= f

synthesizeM' :: forall ki phi codes ix m a
              . (Monad m , IsNat ix)
             => (forall iy a. IsNat iy => Fix ki codes iy -> m a -> m a)
             -> (forall iy  . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy))
             -> Fix ki codes ix
             -> m (AnnFix ki codes phi ix)
synthesizeM' p f = cataM' p alg
  where
    alg :: forall iy
         . (IsNat iy)
        => Rep ki (AnnFix ki codes phi) (Lkup iy codes)
        -> m (AnnFix ki codes phi iy)
    alg xs = flip AnnFix xs <$> f (mapRep getAnn xs)

If we shuffle around the arguments of Rep, it is clear it returns a Functor over Set^n

data RepF :: (kon -> *) -> [[[Atom kon]]] -> (Nat -> *) -> (Nat -> *) where
  RepF :: Rep ki phi (Lkup ix codes) -> RepF ki codes phi ix

then we can use a heterogenous Fix that doesnt mention generics-mrsop constructs at all.
I'm not sure if we actually want it in code, but it's at least a nice comment to show there's
a direct relationship with the Fix that most people already know.

data Fix :: ((Nat -> *) -> (Nat -> *)) -> (Nat -> *) where
  Fix :: f (Fix f) n -> Fix f n


a  ~  Fix (RepF (Code a))

vs

data Fix :: (* -> *) -> * where
  Fix :: f (Fix f) -> Fix f

Usecase: I want to show diffs in my library :)

Also, when experimenting in GHCI it would be super useful to be able to do this:

λ> deep @FamRoseInt ((3::Int) :>: [])

<interactive>:9:1: error:
    • No instance for (Show (Fix Singl CodesRoseInt 'Z))

I can do this in GHC.Generics so i'm pretty sure we can hack something together:

λ> from1 (5::Int) :>: [])
M1 {unM1 = L1 (M1 {unM1 = M1 {unM1 = Par1 {unPar1 = 5}} :*: M1 {unM1 = Comp1 {unComp1 = []}}})}

We should also think about displaying metadata. Maybe we want a separate showWithMeta function for that or whatever?

Looking at f5d6348 , it makes sense to drop Fix altogether.

For that, we'd need a type synonym and a pattern synonym to make the rest of the code
compile as is. @arianvp , feel free to throw in a PR when you're back from holidays!

GHC-head complains about our usage of *.... Hey, GHC, are you for real? LOL

src/Generics/MRSOP/Util.hs:43:23: error:
    Operator applied to too few arguments: *
    With NoStarIsType (implied by TypeOperators), ‘*’ is treated as a regular type operator. 
    Did you mean to use ‘Type’ from Data.Kind instead?
   |
43 | data (:*:) (f :: k -> *) (g :: k -> *) (x :: k)
   |                       ^

Seems like a trivial, but painful fix: We did mean to use Type from Data.Kind GHC. Thanks.

following on #47

I think the ideal would be to have more control over how the names
are generated in the TH interface. for example:

data BlaBla = ...

deriveFamily ''OpqTypes [t| BlaBla |] names

names :: NamingStructure
names = def { familyName = ("BlaBla_" ++)
            , codesName = ("__" ++) 
            , genPatternSyns = True
            }

Originally posted by @VictorCMiraldo in #47 (comment)

The th-abstraction package provides a unified interface for multiple versions of Template Haskell. It might be worth migrating the code to use it, knowing that the template-haskell package changes on every major GHC release.

As soon as you use HasDatatypeInfo, you run into practical issues.

The outer shell is easily inspected, but as soon as you pattern match on your Rep, you don't
have enough information anymore to continue analyzing metadata.
A quick example would be an implementation of the show function:

showFix
  :: forall ki fam codes ix. (Show1 ki, IsNat ix, HasDatatypeInfo ki fam codes ix)
  => Fix ki codes ix
  -> String
showFix (Fix rep) = elimRep show1 showFix mconcat rep

P.S., the above definition only works when we fix #20

The problem is, that the eliminator does not carry enough information

elimRep :: (forall k. ki k -> a) -> (forall k. IsNat k => f k -> a) -> ([a] -> b) -> Rep ki f c -> b

The Fix eliminator (forall k. IsNat k => f k -> a) should have the HasdatatypeInfo constraint,
but that's not easily addable.

Any ideas @VictorCMiraldo ?

You run into similar issues when manually pattern matching :

visualizeNA :: Show1 ki => NA ki (Fix ki codes) a -> Dot NodeId
-- TODO: This recursive call is problematic, as we have no way of infering HasDatatypeInfo
-- as we threw away the `fam` in which the `NA` is present
visualizeNA (NA_I i) = visualizeFix i
visualizeNA (NA_K k) = node [("label", show1 k)]

visualizeFix
  :: forall ki fam codes ix. (Show1 ki, IsNat ix , HasDatatypeInfo ki fam codes ix) 
  => Fix ki codes ix
  -> Dot NodeId
visualizeFix (Fix rep) =
  case sop rep of
    Tag c prod ->
      let
        info = datatypeInfo (Proxy :: Proxy fam) (Proxy :: Proxy ix)
        constrInfo = constrInfoLkup c info
      in do
        constr <- node [("label", constructorName constrInfo)]
        fields <- elimNPM visualizeNA prod 
        traverse (constr .->.) fields
        pure constr

Haskell already has Eq1 and Show1. We should choose different names.
We can call our variants HOEq and HOShow for higher order equality and show.

They don't need type annotations to work, and it makes working with sop function easier!

Basically ,we want to automatically generate this line:

The cleveref provides much better support for references. In particular, it provides \Cref which expands to "Section X", "Theorem X", or whatever is needed.

I open this issue to remember ourselves to change every \ref to \Cref. I've tried for half an hour to use LaTeX macros to do this for us, but I could not 😞