Hi Ken,
ideally, you'd want something like
f1 :: TypeLits.SomeNat -> exists n . Foo n
to indicate that this function will produce a Foo with some natural number,
but you don't know beforehand what that number is.
However, Haskell doesn't have built-in existential quantification (yet), so
you have to use some encoding that uses existing features instead.
There's at least two ways to do this. The first is to use an "existential
data type":
data SomeFoo = forall n . MkSomeFoo (Foo n)
You'll notice that it's named quite similarly to SomeNat - that's because
SomeNat is also an existential data type.
Then you could have a function like
showSomeFoo :: SomeFoo -> String
showSomeFoo (MkSomeFoo x) = show x
The other way is to pass in a function that tells f1 what to do with Foo it
produces:
f1 :: TypeLits.SomeNat -> (forall fn . Foo fn -> a) -> a
f1 mynat f = case mynat of {
TypeLits.SomeNat (_ :: Proxy n) -> let {
x :: Foo n;
x = Mkfoo;
} in f x
};
In this case, you could call `f1 someNat show` to show a Foo made from
someNat.
These two encodings are equally powerful, but sometimes one is more
convenient than the other.
Cheers,
Jakob
On Sat, Feb 20, 2021 at 12:22 PM Ken T Takusagawa
{- I am experimenting with type-level naturals and with moving values known at runtime to type space.
Is there a type signature that I can add to f1 below so that this will compile (maybe also requiring some additional LANGUAGE pragmas)?
If I were to change the return value of f1 from "x" to "show x", then the program does compile, suggesting that there's nothing inherently wrong with "x". But I'd prefer the option to compose the output of f1 with other computations separately, e.g., "show . f1" .
Thanks, Ken
-}
{-# LANGUAGE KindSignatures, ScopedTypeVariables, DataKinds, Rank2Types #-} import qualified GHC.TypeLits as TypeLits; import Data.Proxy(Proxy); main = undefined;
data Foo (fn :: TypeLits.Nat) = Mkfoo deriving (Show);
--f1 :: TypeLits.SomeNat -> ? ; f1 mynat = case mynat of { TypeLits.SomeNat (_ :: Proxy n) -> let { x :: Foo n; x = Mkfoo; } in x };
{- typelits.hs:27:8: error: * Couldn't match expected type `p' with actual type `Foo n' because type variable `n' would escape its scope This (rigid, skolem) type variable is bound by a pattern with constructor: TypeLits.SomeNat :: forall (n :: TypeLits.Nat). TypeLits.KnownNat n => Proxy n -> TypeLits.SomeNat, in a case alternative at smalltypelits2.hs:24:3-33 * In the expression: x In the expression: let x :: Foo n x = Mkfoo in x In a case alternative: TypeLits.SomeNat (_ :: Proxy n) -> let x :: Foo n x = Mkfoo in x * Relevant bindings include x :: Foo n (bound at smalltypelits2.hs:26:5) f1 :: TypeLits.SomeNat -> p (bound at smalltypelits2.hs:23:1) | 27 | } in x | ^ -} _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.