lambdageek / unbound-generics

Specify variable binding in syntax trees using GHC.Generics (reimplementation of Unbound)
https://hackage.haskell.org/package/unbound-generics/
BSD 3-Clause "New" or "Revised" License
56 stars 18 forks source link

Expose GAlpha methods #10

Closed christiaanb closed 9 years ago

christiaanb commented 9 years ago

But only the methods, so that we may use GAlpha without being able to create new bogus instances.

I do this, because my situation is the following. I have a the following data type:

-- | Term representation in the CoreHW language: System F + LetRec + Case
data Term
  = Var     Type TmName                    -- ^ Variable reference
  | Data    DataCon                        -- ^ Datatype constructor
  | Literal Literal                        -- ^ Literal
  | Prim    Text Type                      -- ^ Primitive
  | Lam     (Bind Id Term)                 -- ^ Term-abstraction
  | TyLam   (Bind TyVar Term)              -- ^ Type-abstraction
  | App     Term Term                      -- ^ Application
  | TyApp   Term Type                      -- ^ Type-application
  | Letrec  (Bind (Rec [LetBinding]) Term) -- ^ Recursive let-binding
  | Case    Term Type [Bind Pat Term]      -- ^ Case-expression: subject, type of
                                           -- alternatives, list of alternatives
  deriving (Show,Typeable,Generic)

Where the Type argument of the Prim constructor is simply an annotation. During alpha equivalence testing, I want to omit checking this annotation, and still use the Generic version of alpha-equality testing for the other constructors:

instance Alpha Term where
  aeq' _ (Prim t1 _) (Prim t2 _) = t1 == t2
  aeq' c t1          t2          = gaeq c (from t1) (from t2)
christiaanb commented 9 years ago

Argh, sorry. I wanted to submit a pull-request for "expose GAlpha methods" only. I didn't know that github would be adding later changes to this pull-request.

lambdageek commented 9 years ago

I think GitHub considers commits to the branch of the pull request to be corrections to the original pull request. In any case, I think 12f5dc5 is good. I don't mind re-exposing name2Integer, either (it was exposed in the original unbound library).

As a matter of personal taste, in my projects I usually define a newtype newtype Irrelevant a = Irrelevant { getIrrelevant :: a } and write its aeq' method by hand. But I think able to refer to the type-directed generic versions is reasonable.

I will process this pull request in several hours.

lambdageek commented 9 years ago

Okay, I merged 12f5dc5 and 118d92daf4d5a65d87519b963ac3afdc5f15fa8b cherrypicks the name2Integer stuff, and 11039ee0d827cb8325f5f690d2a2ffe8453f4134 has the name2String fix.

Thanks!