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