Haskell Supertypes and Subtypes-CodePudding

I'm learning Haskell and trying to transcribe a grammar and some subsequent evaluation rules found in a book (TAPL, by Pierce: https://theswissbay.ch/pdf/Gentoomen Library/Maths/Comp Sci Math/Benjamin_C._Pierce-Types_and_Programming_Languages-The_MIT_Press(2002).pdf) on page 48 (and also on page 44 but I compounded them), but I'm running into some troubles. As you may see on pg. 48 (and on 44), the grammar nv is a subset of v and also they're used interspersedly in the semantics, which is what I'm trying to accomplish with the code below:

data Expr = Tr | Fl | IfThenElse Expr Expr Expr | IsZero Expr  | Succ Expr | Pred Expr |Zero
     deriving (Show, Eq)

data V = NV 
    deriving (Show, Eq)

data NV = Zero | Succ NV 
    deriving (Show, Eq)

ssos :: Expr -> Expr
-- PAGE 44
-- E-IFTRUE
ssos (IfThenElse Tr t2 t3) = t2
-- E-IFFALSE
ssos (IfThenElse Fl t2 t3) = t3
-- E-IF
ssos (IfThenElse t1 t2 t3) = let t' = ssos t1 in IfThenElse t' t2 t3
-- PAGE 48
-- E-SUCC
ssos (Succ t1) = let t' = ssos t1 in Succ t'
-- E-PREDZERO
ssos (Pred Zero) = Zero
-- E-PREDSUCC
ssos (Pred (Succ nv1)) = nv1
-- E-PRED
ssos (Pred t1) = let t' = ssos t1 in Pred t'
-- E-ISZEROZERO
ssos (IsZero Zero) = Tr
-- E-ISZEROSUCC
ssos (IsZero (Succ nv1)) = Fl
-- E-ISZERO
ssos (IsZero t1) = let t' = ssos t1 in IsZero t'

And the error is a 'multiple declarations' error which makes sense because I'm defining both Succ and Zero in two separate types, but when I change the names it sort of breaks everything.

Is there a way I can make Succ a type of Expr but also of type NV like it shows in the book?

Thanks!

CodePudding user response：

The best way in Haskell is really to rename constructors differently. Then you get error messages that tell you exactly which names you need to fix.

CodePudding user response：

A possibility is to write a single generic type that can act as either Expr or NV, depending on how you parameterize it:

{-# LANGUAGE DataKinds, KindSignatures, GADTs, StandaloneDeriving #-}

import Data.Kind (Type)

data ExprFlavour = IsExpr | IsNV

type Expr = GenericExpr 'IsExpr
type NV = GenericExpr 'IsNV

data GenericExpr :: ExprFlavour -> Type where
  Tr :: Expr
  F1 :: Expr
  IfThenElse :: Expr -> Expr -> Expr
  IsZero :: Expr -> Expr
  Succ :: GenericExpr flv -> GenericExpr flv
  Pred :: Expr -> Expr
  Zero :: GenericExpr flv
deriving instance Show (GenericExpr flv)

*Main> Succ Zero :: NV
Succ Zero
*Main> Succ Zero :: Expr
Succ Zero
*Main> Succ Tr :: Expr
Succ Tr
*Main> Succ Tr :: NV

:7:1: error:
    • Couldn't match type ‘'IsExpr’ with ‘'IsNV’
      Expected type: NV
        Actual type: GenericExpr 'IsExpr
    • In the expression: Succ Tr :: NV
      In an equation for ‘it’: it = Succ Tr :: NV