FR
PréludeChargé par défaut — aucun import nécessaire.

IsList — overloaded list literals ([..])

Synopsis
interface IsList f where
fromListLit : List a -> f a

The adapter behind a [1, 2, 3] literal whose expected type is a container WITHOUT the constructors ::/Nil. A literal [e1, …, en] IS the cons-spine e1 :: … :: en :: Nil, resolved by the expected type and defaulting to List ; at List or LazyList, which own those constructors, that spine is the value itself (a LazyList literal keeps its tails suspended, as a :: e :: Nil does). At any other container — Vector, Array, yours — the typechecker builds the spine as a List and hands it to fromListLit, which realises it in that container's own representation (Vector : a dense buffer in O(n), never the O(n²) of repeated dense cons). This is the construction half of Haskell's IsList; oppi keeps [..] PATTERNS structural over List (the sole cons instance), so the class needs no nil/cons methods.

The method is fromListLit, NOT fromList: the bare name fromList is already the qualified-module constructor across the stdlib (Vector.fromList, String.fromList, Map.fromList, …) and is used point-free inside the Prelude, so a same-named bare class method would shadow it. Users write the surface [..]; fromListLit is the elaboration target, given here only so a custom container can opt its own [..] literal in.

Instances : LazyList, List, Vector