search

haskus / packages

Haskus packages
https://haskus.org/
24 stars 11 forks source link

constructor removal using splitVariantF ? #7

Closed pcarbonn closed 5 years ago

pcarbonn commented 5 years ago

I'm trying to simplify generic constructor removal like this:

  alg2 x = case splitVariantF @'[EvenF Int, OddF Int] x of
    Left v          -> variantFToCont v >::>
                         ( \(EvenF a l) -> Cons a l
                         , \(OddF a l)  -> Cons a l
                         )
    Right leftovers -> ...

Unfortunately, I can't find a way to leave leftovers unchanged: is there a way out ?

pcarbonn commented 5 years ago

If I say

Right leftovers -> VF leftovers

I get the following error message:

    * Couldn't match type `haskus-utils-types-1.1:Haskus.Utils.Types.List.Index
                             (1
                              GHC.TypeNats.+ (1
                                              GHC.TypeNats.+ haskus-utils-types-1.1:Haskus.Utils.Types.List.IndexOf'
                                                               (VariantF
                                                                  '[ConsF Int, NilF]
                                                                  (EADT '[ConsF Int, NilF]))
                                                               '[]
                                                               '[ConsF
                                                                   Int
                                                                   (Fix
                                                                      (VariantF
                                                                         '[ConsF Int, NilF])),
                                                                 NilF
                                                                   (Fix
                                                                      (VariantF
                                                                         '[ConsF Int, NilF]))]))
                             '[ConsF Int (Fix (VariantF '[ConsF Int, NilF])),
                               NilF (Fix (VariantF '[ConsF Int, NilF]))]'
                     with `VariantF '[ConsF Int, NilF] (EADT '[ConsF Int, NilF])'
      Expected type: VariantF
                       (haskus-utils-types-1.1:Haskus.Utils.Types.List.Filter
                          (OddF Int)
                          (haskus-utils-types-1.1:Haskus.Utils.Types.List.Filter
                             (EvenF Int) '[EvenF Int, OddF Int, ConsF Int, NilF]))
                       (EADT '[ConsF Int, NilF])
        Actual type: haskus-utils-types-1.1:Haskus.Utils.Types.List.Index
                       (haskus-utils-types-1.1:Haskus.Utils.Types.List.IndexOf'
                          (VariantF
                             (haskus-utils-types-1.1:Haskus.Utils.Types.List.Filter
                                (OddF Int)
                                (haskus-utils-types-1.1:Haskus.Utils.Types.List.Filter
                                   (EvenF Int) '[EvenF Int, OddF Int, ConsF Int, NilF]))
                             (EADT '[ConsF Int, NilF]))
                          (ApplyAll (EADT '[ConsF Int, NilF]) '[ConsF Int, NilF])
                          (ApplyAll (EADT '[ConsF Int, NilF]) '[ConsF Int, NilF]))
                       (ApplyAll (EADT '[ConsF Int, NilF]) '[ConsF Int, NilF])
    * In the first argument of `cata', namely `alg2'
      In the expression: cata alg2
      In an equation for `cataAlg2': cataAlg2 = cata alg2
    |
112 |   cataAlg2 = cata alg2
    |                   ^^^^

Not sure how to fix it...

hsyl20 commented 5 years ago

Yes! You can lift a VariantF into another with liftVariantF:

alg2 x = case splitVariantF @'[EvenF Int, OddF Int] x of
    Left v          -> variantFToCont v >::>
                         ( \(EvenF a l) -> Cons a l
                         , \(OddF a l)  -> Cons a l
                         )
    Right leftovers -> Fix (liftVariantF leftovers)

I've updated the doc: https://docs.haskus.org/eadt/constructor_removal.html#generic-input-fixed-matches

pcarbonn commented 5 years ago

Sounds terrific ! This can be used for nanopass in an interpreter.

I get an error when the list of constructor has only one element:

  alg2 x = case splitVariantF @'[EvenF Int] x of
    Left v          -> variantFToCont v >::>
                         ( \(EvenF a l) -> Cons a l
                         )
    Right leftovers -> Fix (liftVariantF leftovers)

Indeed, a tuple cannot have just one element:

    * The lambda expression `\ (EvenF a l) -> Cons a l'
      has one argument,
      but its type `ContListToTuple
                      '[EvenF Int (Fix (VariantF bs))] (Fix (VariantF bs))'
      has none
      In the second argument of `(>::>)',

Maybe we need another operator when there is only one match ?

hsyl20 commented 5 years ago

There are at least two solutions:

1) You can use Single a which is a 1-tuple:

variantFToConf v >::> Single (\(EvenF a l) -> ...)

2) You can use popVariantF instead of splitVariantF + variantFToCont:

alg2 x = case popVariantF @(EvenF Int) x of
   Right (EvenF a l) -> Cons a l
   Left leftovers    -> Fix (liftVariantF leftovers)

I would use the second one.

pcarbonn commented 5 years ago

Sounds good ! Thanks.

pcarbonn commented 5 years ago

Woops, When I try your second solution:

  alg2 x = case popVariantF @(EvenF Int) x of
    Right (EvenF a l) -> Cons a l
    Left leftovers -> Fix (liftVariantF leftovers)

  cataAlg2 :: EADT '[EvenF Int, OddF Int, ConsF Int, NilF]
           -> EADT '[           OddF Int, ConsF Int, NilF]    
  cataAlg2 = cata alg2

I get the following error:

   * Could not deduce: ApplyAll (EADT bs) as0 ~ ApplyAll (EADT bs) as
      from the context: (KnownNat
                           (haskus-utils-types-1.1:Haskus.Utils.Types.List.IndexOf'
                              (ConsF Int (EADT bs))
                              (ApplyAll (EADT bs) bs)
                              (ApplyAll (EADT bs) bs)),
                         KnownNat
                           (haskus-utils-types-1.1:Haskus.Utils.Types.List.IndexOf'
                              (ConsF Int) bs bs),
                         KnownNat
                           (haskus-utils-types-1.1:Haskus.Utils.Types.List.IndexOf'
                              (EvenF Int (EADT bs))
                              (ApplyAll (EADT bs) xs)
                              (ApplyAll (EADT bs) xs)),
                         Haskus.Utils.Variant.PopVariant
                           (ConsF Int (EADT bs)) (ApplyAll (EADT bs) bs),
                         Haskus.Utils.Variant.PopVariant
                           (EvenF Int (EADT bs)) (ApplyAll (EADT bs) xs),
                         Haskus.Utils.Variant.LiftVariant
                           (ApplyAll (EADT bs) as) (ApplyAll (EADT bs) bs),
                         haskus-utils-types-1.1:Haskus.Utils.Types.List.Index
                           (haskus-utils-types-1.1:Haskus.Utils.Types.List.IndexOf'
                              (ConsF Int) bs bs)
                           bs
                         ~ ConsF Int,
                         haskus-utils-types-1.1:Haskus.Utils.Types.List.Index
                           (haskus-utils-types-1.1:Haskus.Utils.Types.List.IndexOf'
                              (EvenF Int (EADT bs))
                              (ApplyAll (EADT bs) xs)
                              (ApplyAll (EADT bs) xs))
                           (ApplyAll (EADT bs) xs)
                         ~ EvenF Int (EADT bs),
                         haskus-utils-types-1.1:Haskus.Utils.Types.List.Filter
                           (EvenF Int (EADT bs)) (ApplyAll (EADT bs) xs)
                         ~ ApplyAll (EADT bs) as,
                         haskus-utils-types-1.1:Haskus.Utils.Types.List.IsMember'
                           (ApplyAll (EADT bs) xs)
                           (EvenF Int (EADT bs))
                           (ApplyAll (EADT bs) xs)
                         ~ 'True,
                         haskus-utils-types-1.1:Haskus.Utils.Types.List.Index
                           (haskus-utils-types-1.1:Haskus.Utils.Types.List.IndexOf'
                              (ConsF Int (EADT bs))
                              (ApplyAll (EADT bs) bs)
                              (ApplyAll (EADT bs) bs))
                           (ApplyAll (EADT bs) bs)
                         ~ ConsF Int (EADT bs),
                         haskus-utils-types-1.1:Haskus.Utils.Types.List.IsSubset as bs
                         ~ 'True)
        bound by the inferred type for `alg2':
                   forall (bs :: [* -> *]) (xs :: [* -> *]) (as :: [* -> *]).
                   (KnownNat
                      (haskus-utils-types-1.1:Haskus.Utils.Types.List.IndexOf'
    ...
pcarbonn commented 5 years ago

I tried with 2.0.3, and I still get the error.

pcarbonn commented 5 years ago

Also, the signature of (both versions of) alg2 is very very long. If I don't write it, I get a warning when -Wall option is activated : Top-level binding with no type signature.

Would it be possible to simplify the signatures, so that I can still use -Wall ?

hsyl20 commented 5 years ago

I have just released haskus-utils-variant 2.1.1 which should fix your issue with popVariantF. It also exports more constraint synonyms so that you can write the types more easily:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeOperators #-}

import Haskus.Utils.EADT hiding (Cons,Nil)
import Haskus.Utils.EADT.TH
import Haskus.Utils.Types.List

data ConsF a e = ConsF a e deriving (Functor)
data EvenF a e = EvenF a e deriving (Functor)
data OddF  a e = OddF a e deriving (Functor)
data NilF    e = NilF      deriving (Functor)

eadtPattern 'ConsF "Cons"
eadtPattern 'EvenF "Even"
eadtPattern 'OddF "Odd"
eadtPattern 'NilF  "Nil"

alg2 ::
   ( ConsF Int :<: ys
   , PopVariantF (EvenF Int) xs (EADT ys)
   , LiftVariantF (Remove (EvenF Int) xs) ys (EADT ys) 
   ) => VariantF xs (EADT ys) -> EADT ys
alg2 x = case popVariantF @(EvenF Int) x of
    Right (EvenF a l) -> Cons a l
    Left leftovers    -> Fix (liftVariantF leftovers)

cataAlg2 :: EADT '[EvenF Int, OddF Int, ConsF Int, NilF]
        -> EADT '[           OddF Int, ConsF Int, NilF]    
cataAlg2 = cata alg2

(Also note that Filter has been renamed into Remove)

pcarbonn commented 5 years ago

Top class ! I have now finalized H-Calc, including an introduction to EADT in the README.

I 'm still struggling finding the correct signature of the alg2 version where the cata recursion-scheme is not used, but that's a minor issue:

  alg4 x = case popVariantF @(EvenF Int) $ unfix x of
    Right (EvenF a l) -> Cons a (alg4 l)
    Left over -> Fix (liftVariantF $ fmap alg4 over)
pcarbonn commented 5 years ago

I don't see anything wrong with this type signature:

  alg4 :: 
    ( ConsF Int :<: ys
    , PopVariantF (EvenF Int) xs (EADT ys)
    , LiftVariantF (Remove (EvenF Int) xs) ys (EADT ys) 
    ) => EADT xs -> EADT ys
  alg4 x = case popVariantF @(EvenF Int) $ unfix x of
    Right (EvenF a l) -> Cons a (alg4 l)
    Left other -> Fix (liftVariantF $ fmap alg4 other)

and yet, I get this error message:

    * Could not deduce: Haskus.Utils.Types.List.IsMember'
                          (ApplyAll (Fix (VariantF xs)) xs)
                          (EvenF Int (Fix (VariantF xs)))
                          (ApplyAll (Fix (VariantF xs)) xs)
                        ~ 'True
        arising from a use of `popVariantF'

Any clue ?

hsyl20 commented 5 years ago

Compared to the catamorphism approach with alg2, here it's a kind of top-down approach hence the functor variable for "PopVariantF" has to be "EADT xs" and not "EADT ys":

alg4 ::
   ( ConsF Int :<: ys
   , PopVariantF (EvenF Int) xs (EADT xs) -- here
   , LiftVariantF (Remove (EvenF Int) xs) ys (EADT ys)
   , Functor (VariantF (Remove (EvenF Int) xs))
   ) => EADT xs -> EADT ys
alg4 x = case popVariantF @(EvenF Int) $ unfix x of
   Right (EvenF a l) -> Cons a (alg4 l)
   Left over         -> Fix (liftVariantF $ fmap alg4 over)