CODEWITHSUNDEEP
haskell
dejsdukes
dejsdukes

Reputation: 121

Haskell Supertypes and Subtypes

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%20Library/Maths/Comp%20Sci%20Math/Benjamin_C._Pierce-Types_and_Programming_Languages-The_MIT_Press%282002%29.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!

Upvotes: 0

Views: 362

Answers (3)

Daniel Wagner
Daniel Wagner

Reputation: 152707

I think the existing answer by leftaroundabout may be a bit more complicated than is intended by that book/makes sense for a beginner. Rather than trying to have a separate type for values, another choice is to simply have a predicate:

isValue :: Expr -> Bool

implemented like:

isValue Tr = True -- from page 44
isValue Fl = True
isValue Zero = True -- from page 48
isValue (Succ e) = isValue e
isValue _ = False

After all, values are not a different kind of beast than expressions; they are expressions, just in one of a few specific shapes.

Your Expr type does not need to change, and V and NV disappear as entities.

Upvotes: 1

leftaroundabout
leftaroundabout

Reputation: 120711

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

Upvotes: 3

Li-yao Xia
Li-yao Xia

Reputation: 33429

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.

Upvotes: 2

Related Questions