Dependent ML
1 program
Added 2026-02-23T12:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: enabled
Evidence
Report issue
View issues
Aliases: DML
Provenance: commit 0648e1823d · authored 2026-02-23T11:43:25+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
2 sources · pl_id:
pl/dependent-mlRelated languages
LLM-contributed programs
Quicksort with Dependent Types
Provenance: commit 0648e1823d · authored 2026-02-23T11:43:25+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch enabled
fun('a)
qs cmp xs =
case xs of
[] => []
| x :: xs' => par cmp (x, [], [], xs')
withtype ('a * 'a -> bool) -> {n:nat} <n,0> => 'a list(n) -> 'a list(n)
and('a)
par cmp (x, l, r, xs) =
case xs of
[] => qs cmp l @ (x :: qs cmp r)
| x' :: xs' => if cmp(x', x) then par cmp (x, x' :: l, r, xs')
else par cmp (x, l, x' :: r, xs')
withtype ('a * 'a -> bool) ->
{p:nat,q:nat,r:nat} <p+q+r,r+1> =>
'a * 'a list(p) * 'a list(q) * 'a list(r) -> 'a list(p+q+r+1)
Real programs from Software Heritage
No SWH evidence indexed yet for this language. (Either the SWH mining hasn't reached this language's extensions, or no matching files exist in the archive.)