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