How can I correctly evaluate this value in my toy language-CodePudding

I'm making a toy language where I want to be able to do arithmetic operations on both Floats and Integers with the same constructors, like so (minimal example provided below).

data Expr a where
  NumberConst :: Number a -> Expr (Number a)
  Mul         :: Expr (Number n) -> Expr (Number n) -> Expr (Number n)

data family Number :: * -> *
data instance Number Integer = NumInt Integer deriving (Eq, Ord, Show)
data instance Number Float   = NumFloat Float deriving (Eq, Ord, Show)

class (Eq a, Ord a, Num a) => SquanchyNum a where

  toDigit  :: Number a -> a
  divide :: Number a -> Number a -> a
  mul    :: Number a -> Number a -> a
  sub    :: Number a -> Number a -> a
  add    :: Number a -> Number a -> a

instance SquanchyNum Integer where

  toDigit  (NumInt x)            = x
  divide (NumInt x) (NumInt y) = x `div` y
  mul    (NumInt x) (NumInt y) = x * y
  sub    (NumInt x) (NumInt y) = x - y
  add    (NumInt x) (NumInt y) = x   y

instance SquanchyNum Float where

  toDigit  (NumFloat x)                = x
  divide (NumFloat x) (NumFloat y) = x / y
  mul    (NumFloat x) (NumFloat y) = x * y
  sub    (NumFloat x) (NumFloat y) = x - y
  add    (NumFloat x) (NumFloat y) = x   y


eval :: Expr a -> a
eval (NumberConst a) = a
eval (Mul a b) = (eval a) `mul` (eval b) <-- this line makes the problem visible

in ghci I get the following error

*Main> :r
[2 of 3] Compiling Lib              ( /home/michael/git/brokensquanchy/src/Lib.hs, 
 interpreted )

/home/michael/git/brokensquanchy/src/Lib.hs:45:18: error:
   • Occurs check: cannot construct the infinite type: n ~ Number n
     Expected type: a
     Actual type: n
• In the expression: (eval a) `mul` (eval b)
  In an equation for ‘eval’: eval (Mul a b) = (eval a) `mul` (eval b)
• Relevant bindings include
    b :: Expr (Number n)
      (bound at /home/michael/git/brokensquanchy/src/Lib.hs:45:13)
    a :: Expr (Number n)
      (bound at /home/michael/git/brokensquanchy/src/Lib.hs:45:11)
|
45 | eval (Mul a b) = (eval a) `mul` (eval b)
   |                  ^^^^^^^^^^^^^^^^^^^^^^^
Failed, one module loaded.

however when I try the following in ghci by hand it works

(eval (NumberConst (NumInt 6))) `mul` (eval (NumberConst (NumInt 2)))
12

This leads me to believe I am not providing enough detail in my type signature for eval. What's the solution?

Edit - I don't think I'm either approaching this problem correctly or explaining it clearly.

Addressing luqui's question

You are already marking the type with the a -- you can deduce from the type which constructor it will be -- the constructor does nothing for you. Why not banish Number a from this source file, just replacing it with a everywhere?

Okay, let's do that with NumberConst

data Expr a where
  NumberConst :: a -> Expr a

Now I can do this

:t NumberConst ("bad code") 
NumberConst ("bad code") :: Expr [Char]

I don't want to be able to do that.

So, I need a way to (1) enforce that my arithmetic constructors can only have an Int or a Float (2) avoid duplicate constructors, one for both Int and Float. I should be able to use arithmetic constructors on either Int or Float. (3) be able to know if it's an Int or a Float so that I can handle division.

A data family plus type class is the way I thought to be able to accomplish that. If that's not necessary, I'm all for a simpler approach. I just don't know what that is.

CodePudding user response：

Okay, let's do that with NumberConst
data Expr a where
 NumberConst :: a -> Expr a
Now I can do this
:t NumberConst ("bad code")
NumberConst ("bad code") :: Expr [Char]
I don't want to be able to do that.

I see. Here we're running a bit into a philosophical question: what is the point of strong types? Many programmers will say, to reject malformed programs. That's certainly an advantage, but Haskell has long followed the direction of what Simon Peyton Jones calls sexy types: a type signature should never just forbid things, but rather guide you so the program is automatically correct.

In other words, restricting what types can be in NumberConst just for the sake of preventing NumberConst "bad code" is not sexy. Instead, you should just require the property that is actually needed. That doesn't require any data families, just simply a typeclass. It seems you basically just require Num / Fractional, except with a division that doubles as div for integral and / for floating types. (Which is maybe not such a good idea BTW, but let's go with it.)

class Num a => Divisible a where
  divide :: a -> a -> a
instance Divisible Int where divide = div
instance Divisible Float where divide = (/)

data Expr a where
  NumberConst :: Divisible a => a -> Expr a
  Mul         :: Expr n -> Expr n -> Expr n

This constraint is enough to prove that every non-infinite Expr a fulfills Divisible a. When you implement eval you'll find that GHC refuses to acknowledge that. As a solution you can either simply add the constraint also to Mul

  Mul         :: Divisible n => Expr n -> Expr n -> Expr n

...which is strictly speaking redundant, but that may not matter; or you can implement a helper function in continuation-passing style that extracts the proof from the expression:

{-# LANGUAGE RankNTypes #-}

evalCPS :: Expr a -> (Divisible a => a -> r) -> r
evalCPS (NumberConst n) q = q n
evalCPS (Mul x y) q = x `evalCPS` \x' -> q $ x' * eval y

eval :: Expr a -> a
eval = evalCPS id

(3) be able to know if it's an Int or a Float so that I can handle division.

The above solution doesn't do that. In fact, anybody could add more instances later on. If you don't want that, if you really want to allow only Int and Float exactly and want to be able to find out which one it is, then I'd suggest you do use separate constructors, but only for the constants:

data Expr a where
  IntConst :: Int -> Expr Int
  FloatConst :: Float -> Expr Float
  Mul :: Expr a -> Expr a -> Expr a

Now, you can again use a CPS version of eval which allows for different continuation depending on whether it's Int or Float:

evalCPSMono :: Expr a -> (Int -> r) -> (Float -> r) -> r
evalCPSMono (IntConst i) qI _ = qI i
evalCPSMono (FloatConst w) _ qF = qF w
evalCPSMono (Mul x y) qI qF
   = evalCPSMono x (\x' -> qI $ x' * eval y)
                   (\x' -> qF $ x' * eval y)

Alternatively, you could express the restriction to exactly two types with a closed type family.

type NumberAllower a where
  NumberAllower Int = Int
  NumberAllower Float = Float
  NumberAllower a = Void

data Expr a where
  NumberConst :: NumberAllower a -> Expr a
  ...

This prevents anybody from writing NumberConst "bad code". But what it does not do is letting you find out what particular type is contained in an Expr. You'd end up having to require that manually from the outside anyway. Not sexy.

An alternative that still has only a single NumberConst constructor, but does let you obtain the exact type, is this (which is perhaps what you tried to write in the first place):

data Number a where
  It'sInt :: Int -> Number Int
  It'sFloat :: Float -> Number Float

data Expr a where
  NumberConst :: Number a -> Expr a
  Mul :: Expr a -> Expr a -> Expr a

This is in practice