Liquid Haskell
1 program
Added 2026-03-10T12:00:00Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: LiquidHaskell
Provenance: commit 671847f653 · authored 2026-03-10T11:08:41+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Safe Operations with Refinement Types
Provenance: commit 671847f653 · authored 2026-03-10T11:08:41+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
{-@ LIQUID "--no-termination" @-}
module SafeOps where
{-@ type Pos = {v:Int | v > 0} @-}
{-@ type NonEmpty a = {v:[a] | len v > 0} @-}
{-@ head' :: NonEmpty a -> a @-}
head' :: [a] -> a
head' (x:_) = x
head' [] = error "unreachable"
{-@ safeDiv :: Int -> {v:Int | v /= 0} -> Int @-}
safeDiv :: Int -> Int -> Int
safeDiv x y = x `div` y
{-@ factorial :: Nat -> Pos @-}
factorial :: Int -> Int
factorial 0 = 1
factorial n = n * factorial (n - 1)
main :: IO ()
main = do
let xs = [1, 2, 3] :: [Int]
putStrLn $ "Head: " ++ show (head' xs)
putStrLn $ "10 / 2 = " ++ show (safeDiv 10 2)
putStrLn $ "5! = " ++ show (factorial 5)