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.