katydid/katydid-haskell

Gadt for expr

Opened this issue · 12 comments

Try refactoring to use GADTs if you want. There are examples on the web of such work. I didn't read deep enough to see if this would be easy or not, but my kneejerk reaction to seeing repetition on ADT for expression is to consider GADTs

I like the extra safety that the ADT is giving me here.
For example the haskell compiler is going to help me not write (And IntExpr DoubleExpr)
While if Expr was a GADT then it would be totally legal and I would have to do that type checking at runtime.
Or am I missing something?

GADT can usually give you the same safety using parameters, but with less repetition. I didn't read your code deeply, it just triggered the reaction that a GADT might fit. If you see something that feels too complicated, stay with what you have. (https://en.wikibooks.org/wiki/Haskell/GADT is the example I was thinking of)

Ok clearly I have not grasped the power of GADTs yet.
Thank you. This is very enlightening.
I'll definitely give it a try.

if you ever apply to Leap Year, they have a really neat exercise, which is what inspired me to read about this... People on Haskell Reddit can give you also sorts of interesting detail about how and when to use GADTs. I am just a novice on the extension/topic.

Very interesting.
Thanks again fro the link, it was a great read.
I have added GADTs, but its not saving me any typing yet.

I have now consolidated my Const constructors into one type.
Now I can see the start of some consolidation.

Once I choose another function to make generic, for example TypesFunc

-    BytesTypeFunc :: Expr Bytes -> Expr Bool
-    BoolTypeFunc :: Expr Bool -> Expr Bool
-    DoubleTypeFunc :: Expr Double -> Expr Bool
-    IntTypeFunc :: Expr Int -> Expr Bool
-    UintTypeFunc :: Expr Uint -> Expr Bool
-    StringTypeFunc :: Expr String -> Expr Bool
+    TypesFunc :: (Eq a) => Expr a -> Expr Bool

then deriving stops working and gives me the following error:

/Users/waschulze/code/src/github.com/katydid/katydid-haskell/src/Expr.hs:124:1: error:
    • Could not deduce: a2 ~ a1
      from the context: (a ~ Bool, Eq a1)
        bound by a pattern with constructor:
                   TypesFunc :: forall a. Eq a => Expr a -> Expr Bool,
                 in an equation for ‘==’
        at src/Expr.hs:124:1-37
      ‘a2’ is a rigid type variable bound by
        a pattern with constructor:
          TypesFunc :: forall a. Eq a => Expr a -> Expr Bool,
        in an equation for ‘==’
        at src/Expr.hs:124:1
      ‘a1’ is a rigid type variable bound by
        a pattern with constructor:
          TypesFunc :: forall a. Eq a => Expr a -> Expr Bool,
        in an equation for ‘==’
        at src/Expr.hs:124:1
      Expected type: Expr a1
        Actual type: Expr a2
    • In the second argument of ‘(==)’, namely ‘b1’
      In the expression: ((a1 == b1))
      In an equation for ‘==’:
          (==) (TypesFunc a1) (TypesFunc b1) = ((a1 == b1))
      When typechecking the code for ‘==’
        in a derived instance for ‘Eq (Expr a)’:
        To see the code I am typechecking, use -ddump-deriv
    • Relevant bindings include
        b1 :: Expr a2 (bound at src/Expr.hs:124:1)
        a1 :: Expr a1 (bound at src/Expr.hs:124:1)

I have also tried it without the Eq a in the type constructor.

I also thought adding constraints would help, but I don't know how? Do you have any tips on how to add constraints to the data type declaration?

Added user defined functions, which is in conflict with this proposal, since it resulted in a rewrite of expressions and they are no longer all in one ADT.
#10