Part2_Sez10_3_hiding

Markdown generated from:
Source idr program: /src/Part2/Sez10_3_hiding.idr
Source lhs program: /src/Part2/Sez10_3_hiding.lhs

Sections 10.3 View APIs. ShapeView example vs Haskell

Type dependent views can be used to provide pattern matching for client code without exposing module implementation details.

Idris code example

module Part2.Sez10_3_hiding

-- export type, not constructors (symilar to typical approach in Haskell)
export
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

-- export these instead of constructors (symilar to typical approach in Haskell)
-- only in Idris we can pattern match on these!
export
triangle : Double -> Double -> Shape
triangle = Triangle

export
rectangle : Double -> Double -> Shape
rectangle = Rectangle

export
circle : Double -> Shape
circle = Circle

-- exports view (with contructors for client to pattern match on) instead of 
-- Shape constructors
-- note exported functions used on the RHS of constructors
public export
data ShapeView : Shape -> Type where
     STriangle : ShapeView (triangle base height)
     SRectangle : ShapeView (rectangle width height)
     SCircle : ShapeView (circle radius)

export
shapeView : (s : Shape) -> ShapeView s
shapeView (Triangle x y) = STriangle
shapeView (Rectangle x y) = SRectangle
shapeView (Circle x) = SCircle

-- example client code 
-- can use elaborate pattern match that reflects on the RHS of ShapeView 
-- using exported functions
area : Shape -> Double
area s with (shapeView s)
  area (triangle base height) | STriangle = 0.5 * base * height
  area (rectangle width height) | SRectangle = width * height
  area (circle radius) | SCircle = pi * radius * radius

{-
*Part2/Sez10_3_hiding> area (circle 1)
3.141592653589793 : Double
-}

Compared to Haskell

Haskell equivalent is not as pretty and not as useful. I am implementing area that works on type level shapes and type level sizes. I am using manually defined fractional type Frac in place of a language built-in Double.
This code does not try to achieve equivalent implementation hiding, rather, it is an experiment in writing a somewhat similar code in Haskell where triangle, rectangle, and circle are used on the type level.

{-# LANGUAGE 
   TemplateHaskell
   , GADTs
   , TypeFamilies
   , DataKinds
   , KindSignatures
   , UndecidableInstances
   , TypeInType
   , ScopedTypeVariables 
#-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module Part2.Sez10_3_hiding where
import Data.Singletons
import Data.Singletons.TH
import Data.Kind (Type)
import Data.Singletons.SuppressUnusedWarnings
import Data.SingBased

$(singletons [d|
  data Shape a = MkTriangle a a
          | MkRectangle a a
          | MkCircle a

  triangle :: a -> a -> Shape a
  triangle = MkTriangle

  rectangle :: a -> a -> Shape a
  rectangle = MkRectangle

  circle :: a -> Shape a
  circle = MkCircle
  
  data Frac = MkFrac Nat Nat deriving Show

  |])

-- | could be placed inside singletons template too
fmulti :: Frac -> Frac -> Frac 
fmulti (MkFrac n1 n2) (MkFrac m1 m2) = MkFrac (multi n1 m1) (multi n2 m2)
  
showFrac :: Frac -> String 
showFrac (MkFrac n m) = show (natToInteger n) ++ "/" ++ show (natToInteger m) 

sF1 = SMkFrac s1 s1 -- `1' as `Sing frac`

ghci:

*Part2.Sez10_3_hiding> :t sF1
sF1 :: Sing ('MkFrac ('S 'Z) ('S 'Z))

Idris' definition of ShapeView translates quite nicely to Haskell.

data ShapeView (s :: Shape a) where
    SvTriangle :: Sing sbase -> Sing sheight -> ShapeView (Triangle sbase sheight)
    SvRectangle :: Sing swidth -> Sing sheight -> ShapeView (Rectangle swidth sheight)
    SvCircle :: Sing sradius -> ShapeView (Circle sradius)

Interestingly, this ShapeView is isomorphic to singletons generated SShape

shapeView :: forall (s :: Shape a) . Sing s -> ShapeView s
shapeView (SMkTriangle a b) = SvTriangle a b
shapeView (SMkRectangle a b) = SvRectangle a b
shapeView (SMkCircle a) = SvCircle a

so using the ShapeView is redundant to the constructs already defined in singletons. Instead of SomeSing Frac I am using the isomorphic Frac directly.

approxPi = MkFrac (integerToNat 22) (integerToNat 7)

area :: forall (s :: Shape Frac) . Sing s -> Frac
area s = case shapeView s of
  SvTriangle sbase sheight -> let fhalf = (MkFrac (integerToNat 1) (integerToNat 2)) 
                              in fhalf `fmulti` (fromSing sbase) `fmulti` (fromSing sheight) 
  SvRectangle swidth sheight -> (fromSing swidth) `fmulti` (fromSing sheight)
  SvCircle sradius -> approxPi `fmulti` (fromSing sradius) `fmulti` (fromSing sradius) 

area' :: forall (s :: Shape Frac) . Sing s -> Frac
area' s = case s of
  SMkTriangle sbase sheight -> let fhalf = (MkFrac (integerToNat 1) (integerToNat 2)) 
                              in fhalf `fmulti` (fromSing sbase) `fmulti` (fromSing sheight) 
  SMkRectangle swidth sheight -> (fromSing swidth) `fmulti` (fromSing sheight)
  SMkCircle sradius -> approxPi `fmulti` (fromSing sradius) `fmulti` (fromSing sradius) 

ghci:

*Part2.Sez10_3_hiding> showFrac $ area' (sCircle sF1)
"22/7"
*Part2.Sez10_3_hiding> showFrac $ area' (sRectangle sF1 sF1)
"1/1"