Unendlich (endlich-periodische) HList in Haskell

Question

Lassen Sie uns sagen, ich habe eine unendliche Folge von Aktionen, von denen jede das Ergebnis eines bestimmten Typs zurückgibt. Etwas wie:

newtype Stream a = Stream (IO (a, Stream a)) 

Aber mit a im Laufe der Zeit verändert. Ich möchte diese Sequenz stark eintippen. Es ist natürlich nicht Sinn für beliebige unendliche Typ-Sequenz und naiven Ansatz machen, so dass:

data HStream :: [u] -> * where Cons :: Proxy x -> HStream xs -> HStream (x ': xs) 

infiniteInt = Cons (Proxy :: Proxy Int) infiniteInt 

zu einer unendlichen Art führen wird, die nicht von Haskell Typ-System unterstützt wird. Aber ich sehe nichts Falsches mit einem endlich-periodischen HLists (d. H. Eine solche welche Art Sequenz wird sich von irgendeinem Punkt wiederholen: [Bool, Int, Int, Sting, Int, Sting, Int, Sting ... ]). Und ich denke auch, dass, wenn wir eine stark normalisierende Weise haben, den unendlichen Typ oder eine Art zu beschreiben, einen Beweis für unendliche Typgleichheit zu liefern, die in einer endlichen Anzahl von Schritten überprüft werden kann, es möglich sein sollte, Programme mit solchen unendlichen Typen zu prüfen.

Hat jemand eine Idee, wie solche Typen in Haskell dargestellt und verwendet werden können? Lasst uns für jetzt von endlos-periodischer hlist ausgehen, aber ich werde es auch schätzen, wenn jemand eine Idee hat, wie es für eine breitere Klasse von unendlichen Tupeln verallgemeinert werden kann und wo Generalisierungsgrenzen liegen.

Answer 1

Machen Sie HList s unendlich und periodisch mit diesem einen coolen Trick!

Wenn Sie Ihrem periodischen heterogenen Stream ein Element hinzufügen, erweitern Sie nicht die Liste der Typen, nach denen es indiziert wird. Drehe es.

type family Append x xs where 
    Append x '[] = '[x] 
    Append x (y ': xs) = y ': Append x xs 

infixr 5 ::: 
data HStream as where 
    (:::) :: { headHS :: a, tailHS :: HStream (Append a as) } -> HStream (a ': as) 

myHStream :: HStream '[Char, Bool, Int] 
myHStream = 'c' ::: True ::: 3 ::: 'x' ::: False ::: -5 ::: myHStream 

Answer 2

Eine allgemeine Möglichkeit von einem HList zu schalten ist, das die Typen aller Elemente codiert, in einen Typ justierten Liste (oder, allgemeiner, eine Art justierten sequence), die entlang Übergängen stellt nur sicher, gültige Pfade

data TAList c x z where 
    Nil :: TAList c x x 
    Cons :: c x y -> TAList c y z -> TAList c x z 

So könnten Sie Ihre Übergänge, mit einiger Sorgfalt kodieren, für x und z eine Möglichkeit große GADT für c und eine geeignete Art von Ihrer Wahl. Infinite type-aligned lists sind kein Problem, da sie in ihrem final type Argument polymorph sind.

Sie könnten wahrscheinlich ein McBride-artiges Indizierungsschema anstelle eines Atkey verwenden, um mehr Flexibilität auf Kosten von mehr Komplexität zu erhalten.