So verwenden Sie den Vergleich in GHC.TypeLits

Question

Ich lief Probleme beim Spielen mit GHC.TypeLits. Betrachten Sie das folgende GADT:

data Foo :: Nat -> * where 
    SmallFoo :: (n <= 2) => Foo n 
    BigFoo :: (3 <= n) => Foo n 

Mein Verständnis war, dass nun für jeden n, der Typ Foo n einen Wert von genau aufgefüllt wird (das entweder ein SmallFoo oder ein BigFoo auf dem Wert von n abhängig).

Aber wenn ich jetzt ein konkretes Beispiel konstruieren wollen, wie folgt:

myFoo :: Foo 4 
myFoo = BigFoo 

Dann GHC (7.6.2) spuckt die folgende Fehlermeldung aus:

No instance for (3 <= 4) arising from a use of `BigFoo' 
Possible fix: add an instance declaration for (3 <= 4) 
In the expression: BigFoo 
In an equation for `myFoo': myFoo = BigFoo 

Dies scheint seltsam - ich erwartet, dass es eine vordefinierte Instanz für solche nat-Vergleiche auf Typenebene gibt. Wie kann ich diese Art von Constraints in meinem Datenkonstruktor mithilfe von Naturals auf Typenebene ausdrücken?

Answer 1

Löser für TypeLists ist nicht in GHC jetzt, nach status page gibt es einige Chancen, dass es in GHC 7.8 im Oktober oder etwas sein wird.

Vielleicht ist es besser, other packages für jetzt zu verwenden.

Answer 2

Dies kompiliert auf dem aktuellen Kopf des type-nats-Zweigs, der (hoffentlich) für 7.8 zusammengeführt werden sollte.

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE FlexibleContexts #-} 
{-# LANGUAGE GADTs #-} 
{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE TypeOperators #-} 

module X where 

import GHC.TypeLits 

data Foo :: Nat -> * where 
    SmallFoo :: (n <= 2) => Foo n 
    BigFoo :: (3 <= n) => Foo n 

myFoo :: Foo 4 
myFoo = BigFoo 

Wo, wenn myFoo geändert wird der Typ sein Foo 1 es, vermutlich weil die x <= y Klasse Zwang erweitert wird auf die (x <=? y) ~ 'True Gleichheit Einschränkung zu kompilieren fehlschlägt:

$ /Source/ghc/inplace/bin/ghc-stage1 /tmp/blah.hs 
[1 of 1] Compiling X    (/tmp/blah.hs, /tmp/blah.o) 

/tmp/blah.hs:16:13: 
    Couldn't match type ‛3 <=? 1’ with ‛'True’ 
    In the expression: BigFoo 
    In an equation for ‛myFoo’: myFoo = BigFoo