haskell - unitarios - vectores en geogebra

Aplicación de una función de vector de longitud fija a la parte inicial de un vector de longitud fija más larga

Question

Tengo la siguiente definición de vectores de longitud fija utilizando las extensiones GADTs , TypeOperators y DataKinds :

data Vec n a where
    T    :: Vec VZero a
    (:.) :: a -> Vec n a -> Vec (VSucc n) a 

infixr 3 :.

data VNat  =  VZero |  VSucc VNat  -- ... promoting Kind VNat

type T1 = VSucc VZero
type T2 = VSucc T1

y la siguiente definición de un TypeOperator :+ :

type family (n::VNat) :+ (m::VNat) :: VNat 
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)

Para que toda mi biblioteca intencional tenga sentido, debo aplicar una función de vector de longitud fija de tipo (Vec nb)->(Vec mb) a la parte inicial de un vector más largo Vec (n:+k) b . Llamemos a esa función prefixApp . Debe tener tipo

prefixApp :: ((Vec n b)->(Vec m b)) -> (Vec (n:+k) b) -> (Vec (m:+k) b)

Aquí hay una aplicación de ejemplo con el change2 función de change2 definido como este:

change2 :: Vec T2 a -> Vec T2 a
change2 (x :. y :. T) = (y :. x :. T)

prefixApp debería poder aplicar change2 al prefijo de cualquier vector de longitud> = 2, por ejemplo

Vector> prefixApp change2 (1 :. 2 :. 3 :. 4:. T)
(2 :. 1 :. 3 :. 4 :. T)

¿Alguien tiene alguna idea de cómo implementar prefixApp ? (El problema es que una parte del tipo de la función de vector de longitud fija debe usarse para tomar el prefijo del tamaño correcto ...)

Edit : la solución de Daniel Wagners (¡muy inteligente!) Parece haber funcionado con algún candidato de lanzamiento de ghc 7.6 (¡no es un lanzamiento oficial!). En mi humilde opinión no debería funcionar, sin embargo, por 2 razones:

1. La declaración de tipo para prefixApp carece de un VNum m en el contexto (para prepend (fb) para verificar correctamente).
2. Aún más problemático: ghc 7.4.2 no asume que TypeOperator :+ sea ​​inyectivo en su primer argumento (ni el segundo, pero eso no es esencial aquí), lo que conduce a un error de tipo: de la declaración de tipo, sabemos que vec debe tener el tipo Vec (n:+k) a y el comprobador de tipos se refiere a la expresión split vec en el lado derecho de la definición a tipo de Vec (n:+k0) a . Pero: el comprobador de tipos no puede inferir que k ~ k0 (ya que no hay seguridad de que :+ sea ​​inyectivo).

¿Alguien sabe una solución a este segundo problema? ¿Cómo puedo declarar que :+ es inyectivo en su primer argumento y / o cómo puedo evitar encontrarme con este problema?

Answer 1

Aquí hay una versión donde la división no está en una clase de tipo. Aquí construimos un tipo de singleton para números naturales (SN), que permite la coincidencia de patrón en `n ''en la definición de división''. Este argumento adicional puede ocultarse mediante el uso de una clase de tipo (ToSN).

La etiqueta de tipo se utiliza para especificar manualmente los argumentos no inferidos.

(Esta respuesta ha sido co-escrita con Daniel Gustafsson)

Aquí está el código:

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, GADTs, ScopedTypeVariables, FlexibleContexts #-}
module Vec where
data VNat = VZero | VSucc VNat  -- ... promoting Kind VNat

data Vec n a where
    T    :: Vec VZero a
    (:.) :: a -> Vec n a -> Vec (VSucc n) a·

infixr 3 :.

type T1 = VSucc VZero
type T2 = VSucc T1

data Tag (n::VNat) = Tag

data SN (n::VNat) where
  Z :: SN VZero
  S :: SN n -> SN (VSucc n)

class ToSN (n::VNat) where
  toSN :: SN n

instance ToSN VZero where
  toSN = Z

instance ToSN n => ToSN (VSucc n) where
  toSN = S toSN

type family (n::VNat) :+ (m::VNat) :: VNat
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)

split'' :: SN n -> Tag m -> Vec (n :+ m) a -> (Vec n a, Vec m a)
split'' Z     _ xs = (T , xs)
split'' (S n) _ (x :. xs) = let (as , bs) = split'' n Tag xs in (x :. as , bs)

split :: ToSN n => Tag m -> Vec (n :+ m) a -> (Vec n a, Vec m a)
split = split'' toSN

append :: Vec n a -> Vec m a -> Vec (n :+ m) a
append T ys = ys
append (x :. xs) ys = x :. append xs ys

prefixChange :: forall a m n k. ToSN n => (Vec n a -> Vec m a) -> Vec (n :+ k) a -> Vec (m :+ k) a
prefixChange f xs = let (as , bs) = split (Tag :: Tag k) xs in append (f as) bs

Answer 2

Hacer una clase:

class VNum (n::VNat) where
    split   :: Vec (n:+m) a -> (Vec n a, Vec m a)
    prepend :: Vec n a -> Vec m a -> Vec (n:+m) a

instance VNum VZero where
    split     v = (T, v)
    prepend _ v = v

instance VNum n => VNum (VSucc n) where
    split   (x :. xs)   = case split xs of (b, e) -> (x :. b, e)
    prepend (x :. xs) v = x :. prepend xs v

prefixApp :: VNum n => (Vec n a -> Vec m a) -> (Vec (n:+k) a -> (Vec (m:+k) a))
prefixApp f vec = case split vec of (b, e) -> prepend (f b) e

Answer 3

Si puedes vivir con un tipo de prefixApp ligeramente diferente:

{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies #-}

import qualified Data.Foldable as F


data VNat  =  VZero |  VSucc VNat  -- ... promoting Kind VNat

type T1 = VSucc VZero
type T2 = VSucc T1
type T3 = VSucc T2

type family (n :: VNat) :+ (m :: VNat) :: VNat
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)

type family (n :: VNat) :- (m :: VNat) :: VNat
type instance n :- VZero = n
type instance VSucc n :- VSucc m = n :- m


data Vec n a where
    T    :: Vec VZero a
    (:.) :: a -> Vec n a -> Vec (VSucc n) a 

infixr 3 :.

-- Just to define Show for Vec
instance F.Foldable (Vec n) where
    foldr _ b T = b
    foldr f b (a :. as) = a `f` F.foldr f b as

instance Show a => Show (Vec n a) where
    show = show . F.foldr (:) []


class Splitable (n::VNat) where
    split :: Vec k b -> (Vec n b, Vec (k:-n) b)

instance Splitable VZero where
    split r = (T,r)

instance Splitable n => Splitable (VSucc n) where
    split (x :. xs) =
        let (xs'' , rs) = split xs
        in ((x :. xs'') , rs)

append :: Vec n a -> Vec m a -> Vec (n:+m) a
append T r = r
append (l :. ls) r = l :. append ls r

prefixApp :: Splitable n => (Vec n b -> Vec m b) -> Vec k b -> Vec (m:+(k:-n)) b
prefixApp f v = let (v'',rs) = split v in append (f v'') rs

-- A test
inp :: Vec (T2 :+ T3) Int
inp = 1 :. 2 :. 3 :. 4:. 5 :. T

change2 :: Vec T2 a -> Vec T2 a
change2 (x :. y :. T) = (y :. x :. T)

test = prefixApp change2 inp -- -> [2,1,3,4,5]

De hecho, su firma original también puede usarse (con contexto aumentado):

prefixApp :: (Splitable n, (m :+ k) ~ (m :+ ((n :+ k) :- n))) =>
             ((Vec n b)->(Vec m b)) -> (Vec (n:+k) b) -> (Vec (m:+k) b)
prefixApp f v = let (v'',rs) = split v in append (f v'') rs

Trabaja en 7.4.1

Actualizaciones: Sólo por diversión, la solución en Agda:

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + r = r
succ n + r = succ (n + r)

data _*_ (A B : Set) : Set where
  _,_ : A -> B -> A * B

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)

split : {A : Set}{k n : Nat} -> Vec A (n + k) -> (Vec A n) * (Vec A k)
split {_} {_} {zero} v = ([] , v)
split {_} {_} {succ _} (h :: t) with split t
... | (l , r) = ((h :: l) , r)

append : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
append [] r = r
append (h :: t) r with append t r
... | tr = h :: tr

prefixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k)
prefixApp f v with split v
... | (l , r) = append (f l) r