idrisidris2

How to use interfaces with parameterized tuple?


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.


Solution

  • 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