I have Coord
function that transforms an n-dimensional size to the type of coordinates bounded by given size: Coord [2,3] = (Fin 2, Fin 3)
.
import Data.Fin
import Data.List
Size : Type
Size = List Nat
Coord : Size -> Type
Coord [] = ()
Coord s@(_ :: _) = foldr1 (,) $ map Fin s
I'd like to use show
and other functions like (==)
with Coord s
:
foo : Coord s -> String
foo x = show x
Error: While processing right hand side of foo. Can't find an implementation for Show (Coord s).
22 | foo : Coord s -> String
23 | foo x = show x
^^^^^^
Earlier I tried to implement Show (Coord s)
, but looks like it's impossible. Here is linked question about it.
You can make your own list like data type:
data Coords : List Nat -> Type where
Nil : Coords []
(::) : Fin x -> Coords xs -> Coords (x :: xs)
toList : Coords xs -> List Nat
toList [] = []
toList (x::xs) = finToNat x :: toList xs
example : Coords [2, 3]
example = [1, 2]
Show (Coords xs) where
show cs = show $ toList cs
You can also try using Data.Vect.Quantifiers.All
or Data.List.Quantifiers.All
:
import Data.Vect
import Data.Vect.Quantifiers
example : All Fin [1, 2, 3]
example = [0, 1, 2]
-- not sure why this is isn't included with Idris
export
All (Show . p) xs => Show (All p xs) where
show pxs = "[" ++ show' "" pxs ++ "]"
where
show' : String -> All (Show . p) xs' => All p xs' -> String
show' acc @{[]} [] = acc
show' acc @{[_]} [px] = acc ++ show px
show' acc @{_ :: _} (px :: pxs) = show' (acc ++ show px ++ ", ") pxs
string : String
string = show example