polyqual.hs

module Poo (nearestCenter) where

import Data.List (minimumBy)

data WrapType b a = WrapType {getVect :: b, getVal :: a}

{-@ type List a N     = {v : [a] | (len v) = N} @-}
{-@ type Point N      = List Double N           @-}
{-@ type GenPoint a N = WrapType (Point N) a    @-}


{-@ nearestCenter :: n:Int -> (GenPoint a n) -> [(Point n)] -> (Point n) @-} 
nearestCenter     :: Int -> WrapType [Double] a -> [[Double]] -> [Double] 
nearestCenter n x = minKey . map (\c -> (c, distance c (getVect x)))

minKey  :: (Ord v) => [(k, v)] -> k
minKey  = fst . minimumBy (\x y -> compare (snd x) (snd y)) 

{- distance :: a:[Double] -> {v:[Double] | (len v) = (len a)} -> Double -}
distance     :: [Double] -> [Double] -> Double 
distance a b = sqrt . sum $ safeZipWith (\v1 v2 -> (v1 - v2) ^ 2) a b

{-@ safeZipWith :: (a -> b -> c) -> xs:[a] -> (List b (len xs)) -> (List c (len xs)) @-}
safeZipWith f (a:as) (b:bs) = f a b : safeZipWith f as bs
safeZipWith _ [] []         = []