An idea of new programming language

Fib.qq

module Main where

dict Integral a = Integral {
  fromInteger: Integer -> a,
  +: a -> a -> a,
  -: a -> a -> a,
  iszero: a -> Bool,
}

impl integralForInteger: Integral Integer
integralForInteger = Integral have
  fromInteger x = x

  x + y = x Main.+ y
  x - y = x Main.- y

  iszero = \
    0 -> True
    _ -> False

fromInteger: forall a. Integral a => Integer -> a
fromInteger %d = d.fromInteger

module Fib begin
  fib: forall a. Integral a => a -> a
  fib @a %d n = go n a0 a1
    where
      a0 = fromInteger %integralForInteger 0
      a1 = fromInteger 1 -- implicit dictionary inference

      -- `go` can have a signature `go: a -> a -> a -> a`
      go m x y = \
        | d.iszero m -> x
        | else       -> go (m - 1) y (x d.+ y)
end

main: IO ()
main = print $ Fib.fib 10

@TheMatten

In many cases, algorithms for undecidable problem are unpredictable; this is from my experience and not principle.

In many cases, decidability in instance search is related compile performance directly.

may have mistake, sorry. Correctly, guarantee of decidability of instance search is important for language designer to maintain the compiler.

Decidability of instance search is more generic concept. A group of instances with cyclic super context is just one of undecidability. Haskell have special syntax for class and instance declaration and the designers of the language thought decidability of instance resolution deeply. Then, undecidable problem of instance resolution in Haskell is just "cyclic context". However, we can choose another design that the instance resolution of our language is turing complete (e.g. arithmetic expression is allowed). This is expressive but compile time depends strongly on the program.

Scala has powerful instance searcher which is a solution of undecidable problem. However, it is a troublemaker for compile performance.