<p>In almost every functional language I know of, quantified type variables are identified using case:</p>
<pre class="lang-haskell prettyprint-override"><code>-- haskell / almost everything miranda-influenced
repl :: a -&gt; Int -&gt; List a
-- quantified vars are lowercase, concrete types/kinds are uppercase
</code></pre>
<p>However, you can do it without case analysis, using explicit quantification:</p>
<pre class="lang-haskell prettyprint-override"><code>-- this also happens to be valid haskell assuming -XRankNTypes
repl :: forall a, a -&gt; Int -&gt; List a
</code></pre>
<p>You then, however, encounter a bit of an issue when making trait/typeclass instance declarations:</p>
<pre class="lang-haskell prettyprint-override"><code>instance Show a =&gt; Show (Maybe a) where
    ...

vs

-- This is not, as far as I know, valid haskell
instance forall a, Show a =&gt; Show (Maybe a) where
    ...
</code></pre>
<p>To be perfectly blunt, that syntax isn't amazing. The actual content, ie <code>Show (Maybe a)</code> gets lost in the requirements and quantification.
However, without using case as a syntactic element, i'm not seeing a better way to do it.
Some things i've considered, but am still open to:</p>
<pre class="lang-haskell prettyprint-override"><code>using `a, ...` === the conventional `forall a, ...` - more unclear
using symbols (ie the actual forall symbol) - more confusing
</code></pre>
<p>I am fully open to a different instance syntax if it helps mitigate this issue.</p>
<p>more info:
My language is close enough to this haskell syntax that any modification to said haskell syntax would transfer over reasonably, so feel free to response in haskell/psudohaskell.</p>

<syntax><functional-programming><traits>
Quantified variables without case-based analysis in traits
CC BY-SA 4.0
2023-06-07T00:24:38.777Z
I think F#'s syntax for this is `'a`, i.e. an identifier preceded by a single quote. If I'm understanding the purpose of this syntax in Haskell (a language I don't use).
kaya3
CC BY-SA 4.0
2023-06-07T00:26:40.283Z
@kaya3 I think that's what MLs do as well? I think the question is about not syntactically differentiating type variables in general (rather than *just* by casing), but that's definitely good to mention.
Unrelated String
CC BY-SA 4.0
2023-06-07T01:11:19.783Z
@UnrelatedString Yes, I would prefer to not disambiguate by any sort of lexical convention, but the `'a` syntax isn't the worst if I don't find a better solution. Thank you both.
blueberry
<p>I suggest &quot;stealing&quot; syntax from <a href="https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html" rel="nofollow noreferrer">Lean 4</a>, it's pretty clean and concise, and doesn't depend on the case of variables or much punctuation:</p>
<pre class="lang-haskell prettyprint-override"><code>class Foo (X : Type) where
  myshow : X -&gt; String

instance [Foo X] [Foo y] : Foo (X × y) where
  myshow x :=
    let ⟨a, B⟩ := x
    &quot;(&quot; ++ Foo.myshow a ++ &quot;, &quot; ++ Foo.myshow B ++ &quot;)&quot;
</code></pre>
<p>I mix cases of both type-level and value-level variables for illustrative purposes.</p>

CC BY-SA 4.0
2023-06-07T17:42:08.223Z
2023-06-07T17:42:08.223Z
Alex Chichigin
# Quantified variables without case-based analysis in traits
Posted by: username_0 on 2023-06-06
In almost every functional language I know of, quantified type variables are identified using case:
-- haskell / almost everything miranda-influenced
repl :: a -> Int -> List a
-- quantified vars are lowercase, concrete types/kinds are uppercase

However, you can do it without case analysis, using explicit quantification:
-- this also happens to be valid haskell assuming -XRankNTypes
repl :: forall a, a -> Int -> List a

You then, however, encounter a bit of an issue when making trait/typeclass instance declarations:
instance Show a => Show (Maybe a) where
    ...

vs

-- This is not, as far as I know, valid haskell
instance forall a, Show a => Show (Maybe a) where
    ...

To be perfectly blunt, that syntax isn't amazing. The actual content, ie Show (Maybe a) gets lost in the requirements and quantification.
However, without using case as a syntactic element, i'm not seeing a better way to do it.
Some things i've considered, but am still open to:
using `a, ...` === the conventional `forall a, ...` - more unclear
using symbols (ie the actual forall symbol) - more confusing

I am fully open to a different instance syntax if it helps mitigate this issue.
more info:
My language is close enough to this haskell syntax that any modification to said haskell syntax would transfer over reasonably, so feel free to response in haskell/psudohaskell.
**Tags:** syntax functional-programming traits
> **Comments:**
> **username_1**: I think F#'s syntax for this is `'a`, i.e. an identifier preceded by a single quote. If I'm understanding the purpose of this syntax in Haskell (a language I don't use).  
> **username_2**: @kaya3 I think that's what MLs do as well? I think the question is about not syntactically differentiating type variables in general (rather than *just* by casing), but that's definitely good to mention.  
> **username_0**: @UnrelatedString Yes, I would prefer to not disambiguate by any sort of lexical convention, but the `'a` syntax isn't the worst if I don't find a better solution. Thank you both.  
---
## 1 answers
### Answer by username_3 on 2023-06-07. Score: 4 | Accepted answer
I suggest "stealing" syntax from Lean 4, it's pretty clean and concise, and doesn't depend on the case of variables or much punctuation:
class Foo (X : Type) where
  myshow : X -> String

instance [Foo X] [Foo y] : Foo (X × y) where
  myshow x :=
    let ⟨a, B⟩ := x
    "(" ++ Foo.myshow a ++ ", " ++ Foo.myshow B ++ ")"

I mix cases of both type-level and value-level variables for illustrative purposes.
---
