haskell dependent-type existential-type

haskell - No se pudo deducir KnownNat en dos existenciales con respecto a la biblioteca singletons



dependent-type existential-type (2)

Necesitas hacer un poco de demostración de teorema para comprobar que, dado KnownNat a y KnownNat b , puedes obtener KnownNat (Min ab) . Una posible solución:

import Data.Constraint

(...)

theorem :: forall a b. (KnownNat a, KnownNat b) => Sing a -> Sing b -> Dict (KnownNat (Min a b)) theorem sa sb = case sCompare sa sb of SLT -> Dict SEQ -> Dict SGT -> Dict fooSing :: forall a. KnownNat a => Foo a -> Sing a fooSing _ = sing minthing'' :: Thing -> Thing -> Integer minthing'' (Thing foo1) (Thing foo2) = case theorem (fooSing foo1) (fooSing foo2) of Dict -> minfoo foo1 foo2

Estaba experimentando con la biblioteca de singletons y encontré un caso que no entiendo.

{-# LANGUAGE GADTs, StandaloneDeriving, RankNTypes, ScopedTypeVariables, FlexibleInstances, KindSignatures, DataKinds, StandaloneDeriving #-} import Data.Singletons.Prelude import Data.Singletons.TypeLits data Foo (a :: Nat) where Foo :: Foo a deriving Show data Thing where Thing :: KnownNat a => Foo a -> Thing deriving instance Show Thing afoo1 :: Foo 1 afoo1 = Foo afoo2 :: Foo 2 afoo2 = Foo athing :: Thing athing = Thing afoo1 foolen :: forall n. KnownNat n => Foo n -> Integer foolen foo = case sing of (SNat :: Sing n) -> natVal (Proxy :: Proxy n) minfoo :: forall a b c. (Min a b ~ c, KnownNat c) => Foo a -> Foo b -> Integer minfoo _ _ = let c = case sing of (SNat :: Sing c) -> natVal (Proxy :: Proxy c) in natVal (Proxy :: Proxy c) thinglen :: Thing -> Integer thinglen (Thing foo) = foolen foo

Podría usar esto para obtener el mínimo de dos cosas

minthing :: Thing -> Thing -> Integer minthing (Thing foo1) (Thing foo2) = min (foolen foo1) (foolen foo2)

Pero ¿por qué no puedo hacer esto?

minthing'' :: Thing -> Thing -> Integer minthing'' (Thing foo1) (Thing foo2) = minfoo foo1 foo2 • Could not deduce (KnownNat (Data.Singletons.Prelude.Ord.Case_1627967386 a a1 (Data.Singletons.Prelude.Ord.Case_1627967254 a a1 (GHC.TypeLits.CmpNat a a1))))


Siento que el comentario de user3237465 debe ser inmortalizado porque elimina la dependencia de la biblioteca de contraint y es bastante prolijo.

minthing'' :: Thing -> Thing -> Integer minthing'' (Thing foo1) (Thing foo2) = theorem (fooSing foo1) (fooSing foo2) $ minfoo foo1 foo2 where fooSing :: KnownNat a => Foo a -> Sing a fooSing = const sing theorem :: forall a b c. (KnownNat a, KnownNat b) => Sing a -> Sing b -> (KnownNat (Min a b) => c) -> c theorem sa sb c = case sCompare sa sb of SLT -> c SEQ -> c SGT -> c