3
$\begingroup$

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.

$\endgroup$
3
  • 3
    $\begingroup$ 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). $\endgroup$ Commented Jun 7, 2023 at 0:24
  • $\begingroup$ @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. $\endgroup$ Commented Jun 7, 2023 at 0:26
  • $\begingroup$ @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. $\endgroup$ Commented Jun 7, 2023 at 1:11

1 Answer 1

Reset to default
4
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.