The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

45417 (1) [Avatar] Offline

When I read the book, I tried answering exercise 2 from section 10.3.4 in the spirit of section 10.3, which is to hide implementation details.

So I kept file Shape_abs.idr as described in the book, and added a ShapeView and associated covering function (with export modifiers):
module Shape_abs

data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

triangle : Double -> Double -> Shape
triangle = Triangle

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

circle : Double -> Shape
circle = Circle

public export
data ShapeView : Shape -> Type where
  STriangle : ShapeView (triangle base height)
  SRectangle : ShapeView (rectangle width height)
  SCircle : ShapeView (circle radius)

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

and then, in the exercise file (ex10_3_4.idr), I wrote (using the usual Type-Define-Refine process) :

import Shape_abs

area : Shape -> Double
area s with (shapeView s)
  area (triangle base height) | STriangle = ?area_rhs_rhs_1
  area (rectangle width height) | SRectangle = ?area_rhs_rhs_2
  area (circle radius) | SCircle = ?area_rhs_rhs_3

However, at this stage, I got a type-checking error : "height is not an accessible pattern variable", and couldn't proceed further.

I saw your solution, which was to define the area function straight after defining the view, but how can I use the view from another module?

Thank you for the wonderful book

439880 (1) [Avatar] Offline
I have got the same error in this exercise. Thanks for the wonderful book.