<p>Long ago, I got <a href="https://stackoverflow.com/q/36002541/1393162">an error message in Scala</a> informing me that I had a GADT skolem. I googled but only found very abstract descriptions of GADT skolems, nothing with an example that illustrated in a realistic context why the concept is needed. I found a workaround to the error but never understood what the trouble. Could you please explain, with a realistic, practical, but hopefully simple example, what is a GADT skolem?</p>

<types><gadt>
What is a GADT skolem?
CC BY-SA 4.0
2023-05-17T16:37:55.440Z
When I saw this question in chat I thought I was in RPG.SE and this is a DnD question
Seggan
CC BY-SA 4.0
2023-05-17T16:39:36.447Z
@Seggan Skolems, not golems.
Ben Kovitz
CC BY-SA 4.0
2023-05-17T16:42:45.567Z
[This SO question](https://stackoverflow.com/questions/12719435/what-are-skolems) may help
user
<p>Say you have an existential type, like this example in Haskell:</p>
<pre><code>-- | A task that will produce a value of type @a@.
data Task a where

  -- | A value of hidden type @t@,
  -- which will be used as input to the task.
  Task :: t -&gt; (t -&gt; IO a) -&gt; Task a
</code></pre>
<p>When you write a function on such a type, you use pattern-matching to bring the type variable <code>t</code> into scope:</p>
<pre><code>runTask :: Task a -&gt; IO a
runTask (Task x f) = f x  -- Here, ‘x :: t’
</code></pre>
<p>Since <code>t</code> is existentially quantified, it should remain abstract—<code>runTask</code> can’t see what type <code>t</code> is.</p>
<p>One way for a compiler to enforce this is by creating a fresh type constant for it, which doesn’t match any other type. This is sometimes referred to as a “skolem constant” or “skolem type variable”, because this process is related to <em>skolemisation</em>, named after logician Thoralf Skolem. (However, typical compilers don’t bother to actually transform the type into skolem normal form, so it may be a bit of a misnomer.)</p>
<p>You may see mention of these variables in an error message if you inadvertently try to use such a type variable outside of its <em>scope</em>. It may be easier to see what this scope is, precisely, if we make it explicit using continuation-passing style:</p>
<pre><code>withTask ::
  Task a -&gt;
  (forall t. t -&gt; (t -&gt; IO a) -&gt; r) -&gt;
  r
withTask (Task x f) k = k x f
</code></pre>
<p>And here’s an example <code>Task</code>:</p>
<pre><code>task :: Task String
task =
  Task
    (42 :: Int)
    \x -&gt; print x *&gt; pure (show x)
</code></pre>
<p>Now, the function we supply as the continuation <code>k</code> cannot make any assumptions about the type <code>t</code>:</p>
<pre><code>-- Error: can’t deduce ‘t ~ Int’
main :: IO ()
main = do
  result &lt;- withTask task \x f -&gt;
    if x == (42 :: Int) then pure &quot;beans&quot; else f x
  putStrLn result
</code></pre>
<p>And also, its return type <code>r</code> cannot mention <code>t</code>:</p>
<pre><code>-- Error: ‘t’ would escape its scope.
stealSecrets task = withTask task \x _f -&gt; x
</code></pre>
<p>Because, in the type of <code>withTask</code>, <code>r</code> is also used as the final return type, which is entirely <em>outside</em> of the scope where <code>t</code> is defined (namely, <code>(forall t. …)</code>). This is also the feature that lets the <code>ST</code> monad enforce the invariant that no <code>STRef</code> escapes the scope of a call to <code>runST</code>, whose type is <code>(forall s. ST s a) -&gt; a</code>.</p>

CC BY-SA 4.0
2023-05-18T00:40:47.400Z
2023-05-18T02:04:46.643Z
2023-05-18T02:04:46.643Z
Jon Purdy
# What is a GADT skolem?
Posted by: username_0 on 2023-05-17
Long ago, I got [an error message in Scala](https://stackoverflow.com/q/36002541/1393162) informing me that I had a GADT skolem. I googled but only found very abstract descriptions of GADT skolems, nothing with an example that illustrated in a realistic context why the concept is needed. I found a workaround to the error but never understood what the trouble. Could you please explain, with a realistic, practical, but hopefully simple example, what is a GADT skolem?
**Tags:** types gadt
> **Comments:**
> **username_1**: When I saw this question in chat I thought I was in RPG.SE and this is a DnD question  
> **username_0**: @Seggan Skolems, not golems.  
> **username_2**: [This SO question](https://stackoverflow.com/questions/12719435/what-are-skolems) may help  
---
## 1 answers
### Answer by username_3 on 2023-05-18. Score: 7
Say you have an existential type, like this example in Haskell:
-- | A task that will produce a value of type @a@.
data Task a where

  -- | A value of hidden type @t@,
  -- which will be used as input to the task.
  Task :: t -> (t -> IO a) -> Task a

When you write a function on such a type, you use pattern-matching to bring the type variable t into scope:
runTask :: Task a -> IO a
runTask (Task x f) = f x  -- Here, ‘x :: t’

Since t is existentially quantified, it should remain abstract—runTask can’t see what type t is.
One way for a compiler to enforce this is by creating a fresh type constant for it, which doesn’t match any other type. This is sometimes referred to as a “skolem constant” or “skolem type variable”, because this process is related to skolemisation, named after logician Thoralf Skolem. (However, typical compilers don’t bother to actually transform the type into skolem normal form, so it may be a bit of a misnomer.)
You may see mention of these variables in an error message if you inadvertently try to use such a type variable outside of its scope. It may be easier to see what this scope is, precisely, if we make it explicit using continuation-passing style:
withTask ::
  Task a ->
  (forall t. t -> (t -> IO a) -> r) ->
  r
withTask (Task x f) k = k x f

And here’s an example Task:
task :: Task String
task =
  Task
    (42 :: Int)
    \x -> print x *> pure (show x)

Now, the function we supply as the continuation k cannot make any assumptions about the type t:
-- Error: can’t deduce ‘t ~ Int’
main :: IO ()
main = do
  result <- withTask task \x f ->
    if x == (42 :: Int) then pure "beans" else f x
  putStrLn result

And also, its return type r cannot mention t:
-- Error: ‘t’ would escape its scope.
stealSecrets task = withTask task \x _f -> x

Because, in the type of withTask, r is also used as the final return type, which is entirely outside of the scope where t is defined (namely, (forall t. …)). This is also the feature that lets the ST monad enforce the invariant that no STRef escapes the scope of a call to runST, whose type is (forall s. ST s a) -> a.
---
